--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on August 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Jessie] loop invariant




On 08/22/2013 04:55 PM, Rovedy Aparecida Busquim e Silva wrote:
> Hi,
> 
> We have a function to be proved (attached).
> 
> To include the code annotations we followed the tutorial
> (www.acm.org/conferences/sac/sac2013/T4-Handout.pdf
> <http://www.acm.org/conferences/sac/sac2013/T4-Handout.pdf>).
> 
> First, we have included the "loop assigns".
> 
> After that, we have tried to include one "loop invariant" for each
> variable of the "loop assigns".
> 
> The analysis of the loop has run without errors when there were not if
> clauses in the code. After including the if clauses the analysis has
> given four errors.

I don't understand what you mean by "without the if clauses". could you
send exactly your other version that has no error ?

Apart from that, there are dubious annotations in your code, see remark
below

> We are using the plugin Jessie, Carbon version.

more than 2 years old, 3 versions appeared after, you should consider
upgrading...

> /*@ loop invariant 0 <= j <= 3;
>     loop invariant soma >= 0.0;  
>     loop invariant \forall integer k; 0 <= k < 3 ==> (soma <= soma +
> acel[k]);                    

this formula is equivalent to

\forall integer k; 0 <= k < 3 ==> (0 <= acel[k]);

is it really what you want to specify ? It doesn't even depend on the
loop variables.

- Claude