--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on September 2015 ---
Hi, Le 02/09/2015 22:10, Kurt Roeckx a écrit : > Hi, > > I'm looking at frama-c to see what I can do with it to, so I ran > it against some code to see what comes out of it. The following > is based on a much larger real file, but I think this already > shows the kind of questions I have. > > I started with the file: > void foo() > { > unsigned int X[16]; > int i; > > for (i = 0; i < 16; i++) > { > X[i] = 0; > } > > for (i = 16; i < 64; i += 8) > { > X[((i+0)+1) & 0x0f]++; > } > } > > (This function of course makes little sense.) > > I run: > frama-c-gui -wp -wp-rte -wp-proof alt-ergo <file> > > Which will then show me: > void foo(void) > { > unsigned int X[16]; > int i; > i = 0; > while (i < 16) { > /*@ assert rte: index_bound: 0 <= i; */ > /*@ assert rte: index_bound: i < 16; */ > X[i] = (unsigned int)0; > /*@ assert rte: signed_overflow: i+1 <= 2147483647; */ > i ++; > } > i = 16; > while (i < 64) { > /*@ assert rte: index_bound: 0 <= (int)((int)((int)(i+0)+1)&0x0f); */ > /*@ assert rte: index_bound: (int)((int)((int)(i+0)+1)&0x0f) < 16; */ > /*@ assert rte: signed_overflow: (int)(i+0)+1 <= 2147483647; */ > /*@ assert rte: signed_overflow: i+0 <= 2147483647; */ > /*@ assert > rte: unsigned_overflow: > X[(int)((int)((int)(i+0)+1)&0x0f)]+1 <= 4294967295; > */ > (X[((i + 0) + 1) & 0x0f]) ++; > /*@ assert rte: signed_overflow: i+8 <= 2147483647; */ > i += 8; > } > return; > } > > And it show me: > [wp] 9 goals scheduled > [wp] [Qed] Goal typed_foo_assert_rte_index_bound_2 : Valid > [wp] [Alt-Ergo] Goal typed_foo_assert_rte_signed_overflow : Valid (16ms) (5) > [wp] [Alt-Ergo] Goal typed_foo_assert_rte_index_bound : Unknown (400ms) > [wp] [Alt-Ergo] Goal typed_foo_assert_rte_signed_overflow_3 : Valid (28ms) (13) > [wp] [Alt-Ergo] Goal typed_foo_assert_rte_signed_overflow_2 : Valid (32ms) (47) > [wp] [Alt-Ergo] Goal typed_foo_assert_rte_signed_overflow_4 : Valid (28ms) (21) > [wp] [Alt-Ergo] Goal typed_foo_assert_rte_index_bound_4 : Unknown (1.4s) > [wp] [Alt-Ergo] Goal typed_foo_assert_rte_index_bound_3 : Unknown (1.5s) > [wp] [Alt-Ergo] Goal typed_foo_assert_rte_unsigned_overflow : Unknown (961ms) > [wp] Proved goals: 5 / 9 > Qed: 1 > Alt-Ergo: 4 (16ms-32ms) (47) (unknown: 4) > > > So I have a some questions about this: > For some reason it can't prove any of the index_bound ones, > except for the 2nd. (i < 16). If I look at the code, they all > seem fairly easy to figure out (for me), since i always has > a clear limit of the values it's going to have. > > Does this require me add things like loop invariants, or something > else? If I add the following before my first for loop it makes > that whole first loop valid: > /*@ loop invariant 0 <= i <= 16; */ Yes, loop invariants are required by deductive proofs. > This all seems to be done by Qed in this case, not alt-ergo. > Why can't alt-ergo figure this out? Is this some shortcomming in > the file that is generated for alt-ergo? Qed is mainly a simplifier. Proof obligation are simplified by Qed before the export to external provers. > Doing the same for the second loop, but then using the following > doesn't seem to help at all: > /*@ loop invariant 16 <= i <= 64; */ The loop invariant is not proved by WP, because it seems to weak. Perhaps, something is missing about the fact that "i" is a 8 multiple (unchecked). > It seems to be unable to prove that, and so the signed overflow checks > that used to be surely_valid are probably turned into the valid_under_hyp > because of that. > > I'm not sure why it can't prove the 3rd index_bound. The only > reason I can think of why it would fail is that it might for some > reason think i could be negative. So I turned it into an unsigned > int, then get to see: > > /*@ assert > rte: index_bound: > (unsigned int)((unsigned int)((unsigned int)(i+(unsigned int)0)+(unsigned int)1)&(unsigned int)0x0f) > < 16; > */ > > And it still unknown, while that should be true for all unsigned integers. Next public version of Frama-C should be able to prove this assertion. Axiomatics about bitwise operations have been improved since the last public release of Frama-C (current non-free version of WP plugin prove it - checked). > Currently a last question is if there is a way to turn off the > unsigned overflow check it adds? I have code that code actually > relies on the overflow behaviour of unsigned integers. The only way I see (unchecked) could be to add the same assertion into your code with a particular tag. //@ assert TheTag: ... ; and add WP plugins to prove all properties exception the one having TheTag (-wp-prop="-TheTag"). The proof of the one coming from the RTE will rely on it. Next, loop invariants about X[i] values have to be given. > Kurt Patrick.