--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on August 2013 ---
Hi, We are sending the working version of the code without the if statements. According to tutorial, we have followed the below sequence: - identify variables modified in the loop: - use loop assigns clause to list variables that (might) have been assigned so far after iterations - define their possible value intervals (relationships) after iterations In our case, we identified the variables j and soma that were modified in the loop. Because of that, we tried to specify the variable soma. Best regards, Nanci, Luciana, Rovedy ---------------------------------------------------------------------------------------- #pragma JessieIntegerModel(math) #pragma JessieTerminationPolicy(user) #pragma JessieFloatModel(math) float acel[3], soma; void test() { int j; acel[0] = 5.0; acel[1] = 5.0; acel[2] = 5.0; soma = 0.0; /*@ loop invariant 0 <= j <= 3; loop invariant soma >= 0.0; loop invariant \forall integer k; 0 <= k < 3 ==> (soma <= soma + acel[k]); loop assigns j, soma; */ for(j=0;j<3;j++) { soma = soma + acel[j]; } } 2013/8/22 Claude Marche <Claude.Marche at inria.fr> > > > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130822/bf46b39e/attachment-0001.html>