--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on May 2011 ---
Idem for the function assigns clause ;) On 03/05/2011 13:43, Zaynah Dargaye wrote: > 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 > > > _______________________________________________ > 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/22b0f38b/attachment.htm>