--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on August 2013 ---
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