Frama-C is proving invalid assertions

Question

I am able to prove the following program using Frama-C, which is surprising because 1) there is an assert false, and 2) the loop invariant does not hold (array a holds 1's not 2's). Am I missing something here?

/*@ requires \valid(a+ (0..9)) && \valid(b+ (0..9));
 */
void test_foo(int *a, char *b) {
  int i = 0;
  /*@ loop invariant \forall int j; 0 <= j < i ==> a[j] == 2; 
      loop invariant \forall int j; 0 <= j < i ==> b[j] == 'a';
   */
  for (int i = 0; i < 10; i++) {
    a[i] = 1;
    b[i] = 'a';
  }   
  //@ assert \false;
}

I am running frama-c as: frama-c -wp -wp-invariants -wp-prover "why3:alt-ergo" -wp-model "Typed,int,real" -wp-par 8 -wp-timeout 15 -wp-out wp.out test.c I see same behavior on both Sodium and Magnesium versions.

Virgile Virgile · Accepted Answer · 2016-01-19T15:39:28

-wp-invariants is not meant to handle "normal" loop invariants such as the ones you have provided, but "general inductive invariants" in the sense of ACSL section 2.4.2. You can thus remove this option from your command line. Then some proof obligations fail as expected.

Note in addition that your loop annotations are incomplete: as warned by WP, you should have a loop assigns, such as

loop assigns i, a[0 .. 9], b[0 .. 9];

Then, in order to be able to prove this loop assigns, you will need to specify i interval of variation:

loop invariant 0<=i<=10;

Finally, the fact that -wp-invariants make proof obligations behave strangely in presence of normal loop annotations should probably be considered as a bug and reported on Frama-C's bts.

Frama-C is proving invalid assertions

1 Answers