--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on July 2020 ---
Can you tell me why the assert at the end of the following pair of nested loops is required to complete the proof. (Try running âframa-c -wp test.c on the attached file test.c.) /*@ requires \valid(dst + (0 .. dstLen-1)); assigns dst[0 .. dstLen-1]; */ void copy2(unsigned * const dst, unsigned const dstLen) { unsigned i = 0; /*@ loop invariant 0 <= i <= dstLen; loop assigns dst[0 .. dstLen-1], i; */ while (i < dstLen) { unsigned j = 0; /*@ loop invariant 0 <= i <= dstLen; loop invariant 0 <= j <= 10; loop assigns dst[0 .. dstLen-1], i, j; */ while (j < 10 && i < dstLen) { dst[i] = 0; i++; j++; } //@ assert \at(dst, Pre) == \at(dst, Here); } } The pointer dst is declared to be a constant pointer. I think it is possible to remove the const-ness with casts, so const doesnât necessarily mean const. But I was surprised that nesting loop invariants of the form âdst == \at(dst, Pre)â or âdst == \at(dst, LoopEntry)â did not solve the problem. The final assert was the only way I could find to complete the proof. Thanks, Mark -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200726/43a05102/attachment-0001.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: test.c Type: application/octet-stream Size: 558 bytes Desc: test.c URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200726/43a05102/attachment-0001.obj>