--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on May 2011 ---
Hi, Your loop assign claus is incomplete, index is also modify in the loop body: loop assign v1[0..index-1], index ; Best On 02/05/2011 18:24, Arnaud Dieumegard wrote: > Hi everyone, > > I'm working on some simple examples but I can't prove the following: > > double v1[2]; > double v2[2]; > > int index; > > /*@ requires \valid_range(v1, 0, 1)&& \valid_range(v2, 0, 1); > assigns v1[0..1]; > ensures \forall integer n; 0<= n< 2 ==> > v1[n] == v2[n]; > */ > void fun(void){ > > //Link invariant from output to Inv > /*@ loop invariant 0<= index<= 2; > loop assigns v1[0..index-1]; > loop invariant \forall integer n; 0<= n< index ==> > v1[n] == v2[n]; > loop variant 2-index; > */ > for(index=0; index<2; ++index){ > v1[index] = v2[index]; > } > } > > Here is the result of the analysis: > > > > > > Does anyone knows why the assign clause is not good ? > Everything works fine without the assign clauses. > > Arnaud > > > > _______________________________________________ > 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/20110503/22085285/attachment.htm>