Frama-C predicates

06 Mar 2020 - tsp
Last update 06 Mar 2020
Reading time 4 mins

As I’ve encountered that many of my friends who also use Frama-C for formal verification of their ANSI C programs really do not know or understand the concept of predicate this is just a short summary. Basically one could imagine a predicate to be a summary of various logical statements that can either hold true or false, i.e. it’s a boolean valued mathematical function that maps to $P : X \to { true, false }$. One can use these predicates to modularize ACSL specifications. They work somewhat like functions with the addition of labels. The most basic predicate is just a collection of simple boolean statements.

Note that this blog post only contains a really basic description of predecates that should be sufficient for most usecases.

For a longer description about Frama-C’s role in formal verification one can look at my previous articles that demonstrated how to do basic verification for simple C programs using the GUI as well as verification of AVR microcontroller code. Predicates are of course also of use in this context.

For a more in-depth introduction one might refer to many other sources like the following:

Simple example

Let’s say we have a structure that wraps an arbitrary number of integer values and we want to define a predicate that specified if this structure is valid or not:

struct bagOfIntegers {
    unsigned long int dwIntegerCount;
    unsigned long int values[];
};

Then one can specify the following predicate to verify that a reference to a bagOfIntegers is valid:

/*@
    predicate bagOfIntegersValid(struct bagOfIntegers *bag) =
        \valid(bag)
        && \valid(&(bag->dwIntegerCount))
        && (bag->dwIntegerCount > 0)
        && \valid(&(bag->values[0..bag->dwIntegerCount-1]));
*/

Now one can annotate set and get functions for this bag using the predicate:

/*@
    requires bagOfIntegersValid(bag) || (bag == \null);
    requires dwIndex >= 0;

    behavior invalidBag:
        assumes (bag == \null);

        assigns \nothing;

        ensures \result == -1;

    behavior invalidIndex:
        assumes bagOfIntegersValid(bag);
        assumes (dwIndex >= bag->dwIntegerCount);

        assigns \nothing;

        ensures bagOfIntegersValid(bag);
        ensures \result == -2;

    behavior validIndex:
        assumes bagOfIntegersValid(bag);
        assumes (dwIndex < bag->dwIntegerCount);

        assigns bag->values[dwIndex];

        ensures bag->values[dwIndex] == value;
        ensures bagOfIntegersValid(bag);
        ensures \result == 0;
*/
int bagOfIntegers_SetEntry(
    struct bagOfIntegers* bag,
    unsigned long int dwIndex,
    unsigned long int value
) {
    if(bag == NULL) {
        return -1;
    }

    if(dwIndex >= bag->dwIntegerCount) {
        return -2;
    }

    bag->values[dwIndex] = value;
    return 0;
}

One might also use such predicates to specify the result of an function, for example an sort function might also specify the sorted predicate:

/*@
    predicate bagOfIntegersSortedASC(struct bagOfIntegers *bag) =
        bagOfIntegersValid(bag)
        && (
            \forall int m; 0 <= m < bag->dwIntegerCount-1
            ==> bag->values[m] < bag->values[m+1]
        ) || (bag->dwIntegerCount < 2);
*/

Labels

Labels are capable of referencing certain positions inside one’s code. They can be used to track memory state. One can specify labels in front of predicate parameters. For example when one wants to specify that variables are swapped after a given set of statements:

/*@
    predicate swappedIntData{L1,L2}(int* data, int len, int i, int j) =
        (i >= 0) && (j >= 0)
        && (i < len) && (j < len)
        && (\at(data[i], L1) == \at(data[j], L2))
        && (\at(data[j], L1) == \at(data[i], L2))
        && (
            \forall int k; (0 <= k < len) && (k != i) && (k != j)
            ==> \at(data[k], L1) == \at(data[k], L2)
        );
*/

One can simply annotate an integer array swapping function:

/*@
    requires \valid(lpData);
    requires (arraySize >= 0);
    requires \valid(&lpData[0..arraySize]);
    requires (i >= 0) && (j >= 0);
    requires (i < arraySize) && (j < arraySize);

    ensures swappedIntData{Old, Here}(lpData, arraySize, i, j);
*/
void intSwap(int* lpData, int arraySize, int i, int j) {
    int temp;

    temp = lpData[i];
    lpData[i] = lpData[j];
    lpData[j] = temp;
}

As usual any label that’s declared in the code (using the usual C labelname: syntax as known as from goto and switch targets) can be used instead of special labels like:

Pre referes to the state at the beginn of function invocation
Old is only valid inside a contract. It referes to the state in which requires and assumes gets evaluated (i.e. the pre-execution state). For a function contract it’s equivalent to the Pre label. For statement contracts this of course adresses the state before execution of the first statement inside the block.
Here is the position at which the annotation get’s evaluated. In contracts this depends on the statement at which it get’s evaluated. Inside an ensures statement it’s equivalent to Post
Post refers to the state at the end of the execution of the contract (and is only valid in ensures, assigns, allocates and frees)
LoopEntry is only valid for loop annotatios and has a similar meaning as Pre for functions.
LoopCurrent adresses the current loop iteration at which the statement gets evaluated.