Frama-C Bug Tracking System - Frama-C
View Issue Details
0001051Frama-CPlug-in > wppublic2011-12-15 18:022011-12-16 17:34
Jochen 
correnson 
normaltextalways
assignedopen 
Frama-C Nitrogen-20111001 
 
0001051: suspicious axiomatization of included,zrange,zunion in .sx file
In 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.
No tags attached.
? store_fill_function_assigns_po_why.sx (40,900) 2011-12-15 18:02
https://bts.frama-c.com/file_download.php?file_id=315&type=bug
? store_swap_ranges_exit_assigns_part3_po_why.sx (41,644) 2011-12-16 17:26
https://bts.frama-c.com/file_download.php?file_id=317&type=bug
Issue History
2011-12-15 18:02JochenNew Issue
2011-12-15 18:02JochenStatusnew => assigned
2011-12-15 18:02JochenAssigned To => correnson
2011-12-15 18:02JochenFile Added: store_fill_function_assigns_po_why.sx
2011-12-16 17:26JochenFile Added: store_swap_ranges_exit_assigns_part3_po_why.sx
2011-12-16 17:34JochenNote Added: 0002557

Notes
(0002557)
Jochen   
2011-12-16 17:34   
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.)