--- layout: fc_discuss_archives title: Message 69 from Frama-C-discuss on August 2013 ---
Hello David, 2013/8/29 David MENTRE <dmentre at linux-france.org>: > > I have tried to use a more detailed memory model with "-wp-model > "Typed,int" " without success. > > I am using Frama-C Fluorine 20130501, Why3 0.81 and Alt-Ergo 0.95.1. > > === > static unsigned char m[] = { > (1 << 7), > (1 << 6), > (1 << 5), > (1 << 4), > (1 << 3), > (1 << 2), > (1 << 1), > (1 << 0) > }; > > /*@ requires n >= 0; > */ > int main(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; > } 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. Options -wp-no-simpl and -wp-nolet do not seem to have an impact on the transformations made by WP. Best regards, -- E tutto per oggi, a la prossima volta Virgile