Frama-C Bug Tracking System - Frama-C
View Issue Details
0001556Frama-CPlug-in > wppublic2013-11-08 17:262014-02-05 15:04
virgile 
correnson 
normalminoralways
acknowledgedopen 
Frama-C GIT, precise the release id 
 
0001556: unprovable PO in function manipulating structs - issue with Qed's simplifications
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.
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.
No tags attached.
? struct_assign.i (353) 2013-11-08 17:26
https://bts.frama-c.com/file_download.php?file_id=596&type=bug
Issue History
2013-11-08 17:26virgileNew Issue
2013-11-08 17:26virgileStatusnew => assigned
2013-11-08 17:26virgileAssigned To => correnson
2013-11-08 17:26virgileFile Added: struct_assign.i
2013-11-08 17:57svnCheckin
2013-11-12 16:44corrensonNote Added: 0004255
2014-02-05 15:04corrensonNote Added: 0004503
2014-02-05 15:04corrensonNote Added: 0004504
2014-02-05 15:04corrensonStatusassigned => acknowledged

Notes
(0004255)
correnson   
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)
(0004503)
correnson   
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.
(0004504)
correnson   
2014-02-05 15:04   
Strategy in Alt-Ergo