Frama-C Bug Tracking System - Frama-C
View Issue Details
0001638Frama-CPlug-in > wppublic2014-02-01 12:492014-07-17 22:21
jens 
correnson 
urgentmajoralways
acknowledgedopen 
Frama-C Fluorine-20130601 
 
0001638: assigns clause appears unprovable
It appears that assigns clauses of functions that modify an array cannot be verified at all. I attach a simple example of a function set_zero that sets all elements of an array to zero (file set_zero.c). Attached is also an attempt to prove the assigns clause with Coq (see file wp0.script). I do not see how from 0 <= n 0 < i one can conclude i <= n Please, correct me if I am totally missing something.
Here is my proof attempt for the assigns clause: Proof. forward. remember a_0 as a. remember n_0 as n. remember i_0 as i. remember Mint_0 as M0. remember Mint_1 as M1. cut (i <= n). auto with zarith. assert(less_equal: 0 <= n). assumption. apply Zle_lt_or_eq in less_equal. rewrite or_comm in less_equal. destruct less_equal as [equal | less]. (* case equal *) rewrite <- equal. assert (~(i <= 0)). auto with zarith. contradict H7. (* what now ? *) Qed.
No tags attached.
related to 0001812acknowledged correnson Assigns not respected in behaviors when using pointers to pointers 
c set_zero.c (409) 2014-02-01 12:49
https://bts.frama-c.com/file_download.php?file_id=656&type=bug
c pb_assigns.c (790) 2014-07-17 22:17
https://bts.frama-c.com/file_download.php?file_id=800&type=bug
Issue History
2014-02-01 12:49jensNew Issue
2014-02-01 12:49jensStatusnew => assigned
2014-02-01 12:49jensAssigned To => correnson
2014-02-01 12:49jensFile Added: set_zero.c
2014-02-05 14:44corrensonNote Added: 0004501
2014-02-05 14:45corrensonNote Added: 0004502
2014-02-05 14:45corrensonStatusassigned => acknowledged
2014-02-06 11:27jensNote Added: 0004515
2014-06-17 11:02corrensonRelationship addedrelated to 0001812
2014-07-17 22:17boulmeFile Added: pb_assigns.c
2014-07-17 22:21boulmeNote Added: 0005270

Notes
(0004501)
correnson   
2014-02-05 14:44   
This is a problem with loop assigns. Current WP strategy avoids taking into account loop invariants for proving loop assigns. I known this is a major drawback, but we can not fix it without refactoring deeply the WP calculus. We are working on this refactoring, but it will not be available for the next release. The workaround is to specify a fixed loop assigns, and use additional invariants to keep what is not modified during the loop if necessary. In the code you submit, simply change loop assigns to a[0..n-1] make everything discharged with Alt-Ergo. In a similar code, eg. swap_ranges or copy, you probably need something like: /*@ ... loop invariant RANGE: 0 <= i <= n ; loop invariant OLD: \forall integer k; i <= k < n ==> a[k] == \at(a[k],Pre); loop assigns a[0..n-1]; */
(0004502)
correnson   
2014-02-05 14:45   
Need wp refactoring.
(0004515)
jens   
2014-02-06 11:27   
Hello Loïc, thank you very much for the explanation and a possible work around. For "ACSL by Example" we will probably stick to our current approach where we use the more specific loop assigns clauses, even if it entails that the assigns clause cannot be verified. Jens
(0005270)
boulme   
2014-07-17 22:21   
Hello Loïc and Jens, I noticed that assigns weaknesses does not only happen with loop assigns, but in some other contexts: see file "pb_assigns.c"