View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
0001556 | Frama-C | Plug-in > wp | public | 2013-11-08 17:26 | 2014-02-05 15:04 | ||||||||
Reporter | virgile | ||||||||||||
Assigned To | correnson | ||||||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||||||
Status | acknowledged | Resolution | open | ||||||||||
Product Version | Frama-C GIT, precise the release id | ||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0001556: unprovable PO in function manipulating structs - issue with Qed's simplifications | ||||||||||||
Description | In the attached file, the two post-conditions KO and OK are equivalent, since s2 is not modified and separated from s1. However, frama-c -wp struct_assign.i shows that WP is only capable to prove OK. | ||||||||||||
Additional Information | the resulting PO for KO is a bit strange. Once all let have been rewritten, it amounts to (in ACSL-like format): \at(s2->x, Pre) == \at(s2->x, Post) Moreover, the state Post is described as the update of the state at L with s1->y |-> \at(s1->y,Pre) + \at(s2->y,L) i.e. as if it wasn't clear whether s1->x and s2->y were separated. If we disable variable elimination, the proof obligation gets discharged by alt-ergo, and there's no mix of memory states in the various updates. Issue is thus likely there. | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files |
|
![]() |
|
correnson (manager) 2013-11-12 16:44 |
The problem rely on the fact that Alt-Ergo gives up exploration as soon as a large constant appears, 2^32. In this case, this prevent it to unfold the definition of separated to find that s1->x and s2->x are different because s1 and s2 are separated. With altgr-ergo (GUI), one can from restrict definition of "def_sint32" to be unfolded, and the POs are discharged immediately. It is also possible to add this assertion at the end of the code: //@ assert SEP: &(s1->x) != &(s2->x) ; [wp] [Qed] Goal typed_f_post_OK : Valid [wp] [Alt-Ergo] Goal typed_f_assign_part1 : Valid (21ms) (23) [wp] [Alt-Ergo] Goal typed_f_assert_SEP : Valid (31ms) (29) [wp] [Alt-Ergo] Goal typed_f_assign_part2 : Valid (Qed:1ms) (18ms) (24) [wp] [Alt-Ergo] Goal typed_f_post_KO : Valid (148ms) (43) [wp] Proved goals: 5 / 5 Qed: 1 (0ms-1ms) Alt-Ergo: 4 (18ms-148ms) (43) Finally, one can also use CVC4: [wp] [Qed] Goal typed_f_post_OK : Valid (1ms) [wp] [cvc4] Goal typed_f_assign_part2 : Valid (60ms) [wp] [cvc4] Goal typed_f_assign_part1 : Valid (60ms) [wp] [cvc4] Goal typed_f_post_KO : Valid (70ms) [wp] Proved goals: 4 / 4 Qed: 1 (0ms-1ms) cvc4: 3 (60ms-70ms) |
correnson (manager) 2014-02-05 15:04 |
Interesting items to send to Alt-Ergo team: (1) frama-c -wp -wp-prover alt-ergo : FAILED (2) frama-c -wp -wp-prover why3:alt-ergo : PASSED Investigating with altgr-ergo shows that the two goals are VERY similar. But in (1), we should deactivate the axioms is_uint32_def1 and/or is_uint32_def2 to prove the goal. The same axioms are present in (2) but they do not borrow alt-ergo. |
correnson (manager) 2014-02-05 15:04 |
Strategy in Alt-Ergo |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2013-11-08 17:26 | virgile | New Issue | |
2013-11-08 17:26 | virgile | Status | new => assigned |
2013-11-08 17:26 | virgile | Assigned To | => correnson |
2013-11-08 17:26 | virgile | File Added: struct_assign.i | |
2013-11-08 17:57 | svn | ||
2013-11-12 16:44 | correnson | Note Added: 0004255 | |
2013-12-20 16:34 | Source_changeset_attached | => frama-clang master 576864e0 | |
2014-02-05 15:04 | correnson | Note Added: 0004503 | |
2014-02-05 15:04 | correnson | Note Added: 0004504 | |
2014-02-05 15:04 | correnson | Status | assigned => acknowledged |