# 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

*Subject*: [Frama-c-discuss] proving assigns*From*: virgile.prevosto at m4x.org (Virgile Prevosto)*Date*: Fri, 18 May 2018 16:07:56 +0200*In-reply-to*: <6EAFA70F-4AE2-4F7D-BB25-847CD591C08E@udel.edu>*References*: <6EAFA70F-4AE2-4F7D-BB25-847CD591C08E@udel.edu>

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>

**Follow-Ups**:**[Frama-c-discuss] proving assigns***From:*siegel at udel.edu (Stephen Siegel)

**References**:**[Frama-c-discuss] proving assigns***From:*siegel at udel.edu (Stephen Siegel)

- Prev by Date:
**[Frama-c-discuss] proving assigns** - Next by Date:
**[Frama-c-discuss] proving assigns** - Previous by thread:
**[Frama-c-discuss] proving assigns** - Next by thread:
**[Frama-c-discuss] proving assigns** - Index(es):