--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on September 2015 ---
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; */ 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? Doing the same for the second loop, but then using the following doesn't seem to help at all: /*@ loop invariant 16 <= i <= 64; */ 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. 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. Kurt