View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
0001051 | Frama-C | Plug-in > wp | public | 2011-12-15 18:02 | 2011-12-16 17:34 | ||||||||
Reporter | Jochen | ||||||||||||
Assigned To | correnson | ||||||||||||
Priority | normal | Severity | text | Reproducibility | always | ||||||||
Status | assigned | Resolution | open | ||||||||||
Product Version | Frama-C Nitrogen-20111001 | ||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0001051: suspicious axiomatization of included,zrange,zunion in .sx file | ||||||||||||
Description | 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. | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files |
|
![]() |
|
Jochen (reporter) 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.) |
![]() |
|||
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 |