In safety-critical software, function pointers should be used sparingly or not at all. They complicate program flow and can make it very hard to understand what the program is doing. However, when used carefully in the right circumstances, they can actually simplify a program.

Typically, function pointers are used in C programs for two different purposes. The first is to connect a generic framework or function to the particular code that is needed in a specific application. The second is to allow a common piece of client code to handle different objects that have a common interface. Both of these can be accomplished in a much more structured way using virtual functions in an object-oriented language (such as C++). But if you’re restricted to C, function pointers offer the only comparable solution available.

Just as pointer arithmetic can be verified if you make some extra effort writing the specifications (see Verifying pointer arithmetic), so can well-designed code using function pointers. In this post I’ll show how you can do this with eCv.

Consider the following code:

typedef int (*myFunc_t)(int);

int foo(int arg)
pre(arg < 100)
post(result > 0);

myFunc_t fptr = &foo;

void test()
{
  int y = 1000/fptr(150);
  ...
}

Can you see the problems? Variable fptr is holding the address of function foo when we make the call fptr(150). However, foo has a precondition that its argument must be less than 100. So in calling fptr(150) we are violating the precondition of foo. Even if we change the call to fptr(50), without knowing that fptr(50) returns a nonzero value, eCv can’t prove that a divide-by-zero error will not occur when we divide 1000 by the result of the call.

eCv solves these problems by making the function specification part of the type. Here’s a verifiable version:

typedef int (*myFunc_t)(int z)
pre(z < 100)
post(result > 0);

int foo(int arg)
pre(arg < 100)
post(result > 0);

myFunc_t fptr = &foo;

void test()
{
  int y = 1000/fptr(50);
  ...
}

Now, when eCv sees the call fptr(50), it knows that whatever function is assigned to fptr requires precondition argument < 100 so it must prove that this is satisfied. Likewise, eCv knows that whatever function is assigned to fptr, it always returns a value greater than zero; so a divide-by-zero error cannot occur in the expression 1000/fptr(50).

However, “There ain’t no such thing as a free lunch”, as the saying goes. The cost of attaching pre- and post-conditions to the type myfunc_t is that we must ensure that whenever we assign the address of a function to fptr, the specification of that function is compatible with the pre- and post-condition of the type myfunc_t. In the example above, the pre- and post-condition of foo are identical to the pre- and post-condition of myfunc_t. But do the specifications always have to be identical, or can we have some leeway?

Suppose we have the following:

typedef int (*myFunc_t)(int z)
pre(z < 100)
post(result > 0);

myFunc_t fptr = ...

int foo2(int arg)
pre(arg < 200)
post(result > 10);

int foo3(int arg)
pre(arg < 50)
post(result > -5);
...
fptr = &foo2;  /* is this valid? */
...
fptr = &foo3;  /* is this valid? */

Let’s first consider the assignment fptr = &foo2. When eCv sees a call of the form fptr(x), it knows from the type of fptr that we have to satisfy precondition x < 100 and that the return value satisfies result > 0.

However, function foo2 has a weaker precondition, because it only requires its argument to be less than 200. So any call that satisfies the precondition of myfunc_t also satisfies the precondition of foo2. Conversely, foo2 has a stronger postcondition, because it guarantees to return a value greater than ten. Any value greater than ten is also greater than zero, so this is fine.

Now let’s look as the assignment fptr = &foo3. Function foo3 has a stronger precondition than myfunc_t – it requires its argument to be less than 50 rather than less than 100. So a call fptr(75) would violate the precondition of foo3, if fptr points to foo3 at the time. Also, foo3 has a weaker postcondition – it only promises to return a value greater than -5, rather than a value greater than 0 as promised by myfunc_t. So a program that calls fptr(x) and assumes the return value will be greater than 0 might fail, because foo3(x) could return (say) -2. Therefore, foo3 fails to be a suitable target for fptr on two counts.

In general, whenever you assign a value of function pointer type, the value on the right hand side of the assignment may validly be a pointer to a function with the same or weaker precondition than the type of the variable you are assigning, and the same or stronger postcondition. The same rule applies when you pass a function pointer as a parameter, when you return a function pointer from a function, and when you use a function pointer to initialize a variable. In object-oriented languages, the same principle applies when a derived class overrides a function defined in a parent class – look up Liskov Substitution Principle if you want to learn more.

eCv supports formal verification of programs using function pointers by generating verification conditions that are true if and only if you have followed these rules, and passing them to the prover along with all the others.

   List of Articles     TOP