Frama-C Bug Tracking System - Frama-C
|View Issue Details|
|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|
|Assigned To||correnson|| |
|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.|
|Steps To Reproduce|
|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|| struct_assign.i (353) 2013-11-08 17:26|
|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-12 16:44||correnson||Note Added: 0004255|
|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|
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)
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.