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] proving assigns

Hello,

2018-05-18 15:01 GMT+02:00 Stephen Siegel <siegel at udel.edu>:

>
> I’m trying to prove the following program, assign.c, with Frama-C/WP :
>
> /*@ requires n>=0;
>   @ requires \valid(a+(0..n-1));
>   @ assigns \nothing;
>   @*/
> void f(int *a, int n) {
>   /*@ loop invariant i1: 0<=i<=n;
>     @ loop assigns i;
>     @*/
>   for (int i=0; i<n; i++) {
>     if (a[i]==2) {
>       a[i]=1;
>       a[i]=2;
>     }
>   }
> }
>
> My understanding of the semantics of “assigns” is that every variable not
> listed in the assigns clause has the same value in the post-state that it
> had in the pre-state.   Similarly for “loop assigns”.   Therefore the
> contract should be valid.  However, I can’t find any combination of
> additional assertions or loop invariants that will prove the program.
>  Maybe I am missing something or have the semantics wrong?
>
>
Your interpretation of ACSL's semantics is perfectly correct. Sadly for
you, WP uses an over-approximation of this semantics when it comes to
generating proof obligations related to assigns clauses (including loop
assigns of course). Basically, it checks that every write access is done on
a location included in the corresponding assigns clause. This is much
easier than quantifying over all memory locations that are valid in
pre-state to check that if they're not in the assigns, then their value
does not change. As a work around, it is possible to put the locations
written to in the assigns clause, with a post-condition/loop invariant
indicating that even though there's a write operation, it has retained its
old value:

/*@ requires n>=0;
    requires \valid(a+(0..n-1));
    assigns a[0 .. n-1];
    ensures \forall integer k; 0<= k < n ==> a[k] == \at(a[k],Pre);
*/
void f(int *a, int n) {
  /*@ loop invariant i1: 0<=i<=n;
      loop assigns i, a[0 .. n-1];
      loop invariant \forall integer k; 0<= k < n ==> a[k] == \at(a[k],Pre);
  */
  for (int i=0; i<n; i++) {
    if (a[i]==2) {
      a[i]=1;
      a[i]=2;
    }
  }
}

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180518/98705d0d/attachment.html>