--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on July 2020 ---
Hi How much time did you allow the provers to spend at most? Assertions can often speed up proofs because of the "narrowing" they do of the set of valid predicates. You might want to look at generating proof scripts with frama-c-gui, and keep track of the saved scripts along with the rest of the code (using say git). /Tomas sön 2020-07-26 klockan 20:31 +0000 skrev Tuttle, Mark: > 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 > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss