Search code examples
static-analysisframa-c

Frama-c WP and preconditions

I have two questions regarding preconditions and Frama-c wp :

  1. How does Frama-c prove preconditions ?
  2. When does Frama-c try to prove preconditions ?

I'm asking these questions because sometimes frama-c wp doesn't even attempt the proof, sometimes it succeeds in proving the precondition and sometimes it fails for example here in the first screenshot the proof wasn't tried

enter image description here

But in this second screenshot we attempted the proof and we failed

enter image description here

I'm assuming that the main function had its effect on that, but is it the full picture ? are preconditions subject of proof only when the function is main ?

Solution

  • As a preliminary, just let me precise that there will be no definite answer to the questions "How/When does Frama-C prove preconditions". More precisely, this is highly dependent on the plug-in(s) you're using. Since you mention WP, I will focus on it.

    In the general case, pre-conditions of a function f are supposed to hold at each call site (that's where the notion of function contract comes from: f guarantees that the post-conditions hold when it returns only to callers that can guarantee that the pre-conditions hold before the call). Hence, if you don't have any call to f in the functions you choose to prove, no proof of the preconditions will be attempted.

    Now, there's an exception for the main function (or more precisely the function designated by the -main option of Frama-C, which defaults to main), as it is supposed to be the entry point of the program, and usually not called anywhere else, an attempt is made to check that the initial program state (where all global variables are equal to their initial value, and formals can have any value) respect the precondition. Note that option -lib-entry indicates that the assumption about global variables having their initial value should not hold, and in that case WP will not attempt to prove the preconditions of the main function, since it cannot make any assumption about its calling context. As an example, the following code:

    int X = 1;

/*@ requires X == 1;
    ensures \result == 1;
*/
int f() { return X; }

    will give 2 (valid) proof obligations with frama-c -wp -main f file.c, and only 1 with frama-c -wp -main f -libentry file.c