2021-01-15 19:34 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001556Frama-CPlug-in > wppublic2013-11-08 17:262014-02-05 15:04
Reportervirgile 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
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 - 
    struct S { int x; int y; };

/*@ requires \separated(s1,s2);
    requires \separated(&s1->x,&s2->y);
    requires 0<=s1->x<=10 && 0<=s2->x<=10;
    ensures KO: s1->x == \old(s1->x) + s2->x;
    ensures OK: s1->x == \old(s1->x) + \old(s2->x);
    assigns s1->x,s1->y;
*/
void f(struct S* s1, struct S* s2) {
  s1->x += s2 -> x;
 L:
  s1->y += s2 -> y;
}
    ? file icon struct_assign.i (353 bytes) 2013-11-08 17:26 +

-Relationships
+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
+Notes

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