--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on September 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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