--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on July 2020 ---
Hi, I donât really understand the problem. Without any assertion, I get instant proof for all loop invariants: $ ./bin/frama-c -wp ~/work/foo.i [kernel] Parsing /Users/correnson/work/foo.i (no preprocessing) [wp] Warning: Missing RTE guards [wp] 12 goals scheduled [wp] [Cache] found:4 [wp] Proved goals: 12 / 12 Qed: 8 (0.93ms-5ms-12ms) Alt-Ergo 2.0.0: 4 (16ms-30ms) (65) (cached: 4) L. > Le 26 juil. 2020 à 22:31, Tuttle, Mark <mrtuttle at amazon.com> a écrit : > > 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 > <test.c>_______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr <mailto:Frama-c-discuss at lists.gforge.inria.fr> > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss <https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss> -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200727/c3602352/attachment-0001.html>