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

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