# Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# [Frama-c-discuss] Simple loop, overflow and bounds

*Subject*: [Frama-c-discuss] Simple loop, overflow and bounds*From*: kurt at roeckx.be (Kurt Roeckx)*Date*: Wed, 2 Sep 2015 22:10:30 +0200

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

**Follow-Ups**:**[Frama-c-discuss] Simple loop, overflow and bounds***From:*Patrick.Baudin at cea.fr (BAUDIN Patrick)

**[Frama-c-discuss] Simple loop, overflow and bounds***From:*dmentre at linux-france.org (David MENTRE)

- Prev by Date:
**[Frama-c-discuss] Speedup Frama-C/WP generating proof obligations** - Next by Date:
**[Frama-c-discuss] Simple loop, overflow and bounds** - Previous by thread:
**[Frama-c-discuss] Speedup Frama-C/WP generating proof obligations** - Next by thread:
**[Frama-c-discuss] Simple loop, overflow and bounds** - Index(es):