Why does WP care about main?

Question

In the following minimal example (slightly altered from Allan Blanchard's excellent tutorial -- section 3.2.3.3 Side Effects):

int h = 42;

/*@
  requires \valid(a) && \valid(b);
  requires \valid_read(a) && \valid_read(b);
  ensures *a == \old(*b) && *b == \old(*a);
 */
void swap( int *a, int *b) {
    int tmp = *a;
    *a = *b;
    *b = tmp;
}

//int test_swap(void) {
int main(void) {
    int a = 37;
    int b = 91;

    //@ assert h == 42;
    swap(&a, &b);
    //@ assert h == 42;
  return 0;
}

With this code as is above, WP is able to prove the first //@ assert h == 42; in main as expected from the discussion in the tutorial.

IF the function main is renamed test_swap WP is un-able to prove the first //@ assert h == 42;

Why?

I can understand why EVA cares about the presence of main, but I can not understand why WP should even care, as I am only asking WP to prove the single function main (in one case) and test_swap (in the other case).

---

I am using Frama-C version: 25.0-beta (Manganese)

Answer 1

By default, Frama-C indeed assumes (at kernel level) that the main function is the entry point of the program. That means that WP can make some assumptions about the global context (basically the initial values of global variables), but also that we might have additional verification to perform on the function. For example, here, we could write:

//@ requires 0 <= h <= 100 ;
int main(void) {
  ...
}

In such a case, WP generates a VC for the requires of the main function and proves it:

If one really wants a behavior where the main function is just handled as any other function, the Frama-C kernel must be parameterized with the -lib-entry option. In such a case:

• WP does not try to prove the requires of main,
• WP cannot prove that h is 42 in the first assert.

frama-c-gui b.c -lib-entry -wp