--- layout: fc_discuss_archives title: Message 72 from Frama-C-discuss on August 2013 ---
Hello Virgile, 2013/8/29 Virgile Prevosto <virgile.prevosto at m4x.org>: > I'm afraid that WP tries to play it a bit too smart here: if you look > at the generated goal, you'll see that the values of the m[i] have > been const-folded, so that you have m[0] == 128, m[1] == 64, etc. It > makes the assert on m[0] trivial, but > the assert on m[bit] much more complicated, as the prover somehow has > to revert back the transformation. Since we're dealing with a bitwise > rather than an arithmetic operation, I'm not sure that there's an easy > way to have alt-ergo prove that. Argh!! Thank you for the explanation! I found an overkill way to prove the property by building it manually and putting it as requirement of the function of interest (see below). I also need to call WP with -wp-model "Typed,int". Even if now everything is proved, this is ugly and much less readable than the original program. :-( I also thought of combining Value analysis and WP to do the same kind of thing as below program, but using Value to prove the property on the static version of m[]. Unfortunately, Value seems unable to reason on \forall quantifier and I see no other way to express the property. A third approach would be to attach a global invariant to the static m (and still require the property at f() entrance): global invariant my_m: \forall integer i; 0 <= i < 8 ==> m[i] == (1 << (7-i)); Unfortunately, WP does not seem to support it (and probably would have the same issue to prove it). ==== unsigned char m[8]; /*@ requires n >= 0; requires \forall integer i; 0 <= i < 8 ==> m[i] == (1 << (7-i)); */ int f(int n) { int size, bit; size = 8; bit = n%size; //@ assert 0 <= bit <= 7; //@ assert m[0] == ((unsigned char)(1 << 7)); //@ assert m[bit] == ((unsigned char)1 << (7-(n%8))); return 0; } int main(int n) { int i; if (n < 0) return -1; /*@ loop invariant 0 <= i <= 8; loop invariant \forall integer j; 0 <= j < i ==> m[j] == (1 << (7-j)); loop invariant n >= 0; */ for (i=0; i<8; i++) { m[i] = (1 << (7-i)); } //@ assert \forall integer i; 0 <= i < 8 ==> m[i] == (1 << (7-i)); f(n); return 0; } ==== Best regards, david