David Crocker's Verification Blog

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. Read more…