View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
0001638 | Frama-C | Plug-in > wp | public | 2014-02-01 12:49 | 2014-07-17 22:21 | ||||||||
Reporter | jens | ||||||||||||
Assigned To | correnson | ||||||||||||
Priority | urgent | Severity | major | Reproducibility | always | ||||||||
Status | acknowledged | Resolution | open | ||||||||||
Product Version | Frama-C Fluorine-20130601 | ||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0001638: assigns clause appears unprovable | ||||||||||||
Description | 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. | ||||||||||||
Additional Information | 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. | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files |
|
![]() |
||||||
|
![]() |
|
correnson (manager) 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]; */ |
correnson (manager) 2014-02-05 14:45 |
Need wp refactoring. |
jens (reporter) 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 |
boulme (reporter) 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" |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2014-02-01 12:49 | jens | New Issue | |
2014-02-01 12:49 | jens | Status | new => assigned |
2014-02-01 12:49 | jens | Assigned To | => correnson |
2014-02-01 12:49 | jens | File Added: set_zero.c | |
2014-02-05 14:44 | correnson | Note Added: 0004501 | |
2014-02-05 14:45 | correnson | Note Added: 0004502 | |
2014-02-05 14:45 | correnson | Status | assigned => acknowledged |
2014-02-06 11:27 | jens | Note Added: 0004515 | |
2014-06-17 11:02 | correnson | Relationship added | related to 0001812 |
2014-07-17 22:17 | boulme | File Added: pb_assigns.c | |
2014-07-17 22:21 | boulme | Note Added: 0005270 |