--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on May 2011 ---
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: -------------- next part -------------- A non-text attachment was scrubbed... Name: PastedGraphic-1.tiff Type: image/tiff Size: 83208 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110502/b25b706d/attachment-0001.tiff> -------------- next part -------------- Does anyone knows why the assign clause is not good ? Everything works fine without the assign clauses. Arnaud