--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on July 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Nested loops



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>