2021-01-16 21:29 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001051Frama-CPlug-in > wppublic2011-12-16 17:34
Assigned Tocorrenson 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in Version 
Summary0001051: suspicious axiomatization of included,zrange,zunion in .sx file
DescriptionIn the attached proof obligations file "store_fill_function_assigns_po_why.sx" generated by Wp for Simplify, I found some Why axioms looking suspicious. Someone should confirm that their current form is intended. For readability, I transform to Acsl and infix when referring to (sub)formulas.

In axiom "inc_range_range", the conjunct "d<=d+sz" could be simplified to "0<=sz"; similar for "b+sz<0" in axiom "inc_range_empty". In the 1st formula of axiom "inc_union_left" (but not in "inc_union_right"), the "==>" could be sharpened to "<==>". Axiom "inc_sub_zone" could be generalized to "\forall z; (z zunion z) included z". Axiom "inc_permut2" is a consequence of idempotence, associativity, and commutativity of zunion; similar for "union_assoc2"; both axioms look very particular.

Possibly, some above suggestions may cause problems to the provers; e.g. axiomatizing zunion's commutativity probably will. However, some suggestions might yet be useful, I hope.
TagsNo tags attached.
Attached Files




Jochen (reporter)

The obligation in file "store_swap_ranges_exit_assigns_part3_po_why.sx" cannot be proven by Simplify when any of the axioms "union_sym", "union_assoc", and "inc_sub_zone" is present; all referring to properties of zunion. If all three axioms are commented out, the proof is found in <1sec.

(Seemingly, in many cases where code can be verified by Jessie, but not by Wp, obligations concerned with memory locations, zrangs, zunion etc. are involved. Therefor it might be worthwile to think about alternative axiomatizations, or at least to know which axioms cause problems.)

-Issue History
Date Modified Username Field Change
2011-12-15 18:02 Jochen New Issue
2011-12-15 18:02 Jochen Status new => assigned
2011-12-15 18:02 Jochen Assigned To => correnson
2011-12-15 18:02 Jochen File Added: store_fill_function_assigns_po_why.sx
2011-12-16 17:26 Jochen File Added: store_swap_ranges_exit_assigns_part3_po_why.sx
2011-12-16 17:34 Jochen Note Added: 0002557
+Issue History