Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001556Frama-CPlug-in > wppublic2013-11-08 17:262014-02-05 15:04
Reportervirgile 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0001556: unprovable PO in function manipulating structs - issue with Qed's simplifications
DescriptionIn 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 Informationthe 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.
TagsNo tags attached.
Attached Files? file icon struct_assign.i [^] (353 bytes) 2013-11-08 17:26 [Show Content]

- Relationships

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

 Strategy in Alt-Ergo

- Issue History
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 Checkin
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

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker