--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on May 2018 ---
[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>