Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Nested loops

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