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