--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on September 2015 ---
Hello, Le 02/09/2015 22:10, Kurt Roeckx a écrit : > 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; */ Exactly! WP does not infer loop bounds. Jessie (other deductive verification plug-in in Frama-C) and GNATprove (for SPARK 2014 in GNAT tool) do it (probably with limitations). > 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? Its simply because Qed is called before Alt-Ergo, to very quickly solve easy goals internally. > 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 think this is due to the use of bit operations ('& 0x0f'). WP is known to be lacking in that regard. I tried to use a more elaborated memory model with '-wp-model Typed+cint+ref+cast' without success. But you would have much more success with Value analysis to prove absence of Run Time Error: $ frama-c -val -slevel 64 -main foo roeckx-loops.c [...] roeckx-loops.c:6:[value] Loop invariant got status valid. roeckx-loops.c:12:[value] Loop invariant got status valid. [value] Recording results for foo [value] done for function foo [value] ====== VALUES COMPUTED ====== [value] Values at end of function foo: X[0] â {0} [1] â {3} [2..8] â {0} [9] â {3} [10..15] â {0} i â {64} > 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. I would say that if WP cannot prove the index increment part, it has not enough hypotheses to prove the loop bounds. > 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. It should be -no-warn-unsigned-overflow option but apparently it does not work. Best regards, david