ID0001051: **This issue was created automatically from Mantis Issue 1051. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001051 | Frama-C | Plug-in > wp | public | 2011-12-15 | 2011-12-16 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open | | **Priority** | normal | **Severity** | text | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - | ### 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. ## Attachments - [store_fill_function_assigns_po_why.sx](/uploads/109e2e7e07696cc6d3f4157468ea5cba/store_fill_function_assigns_po_why.sx) - [store_swap_ranges_exit_assigns_part3_po_why.sx](/uploads/f1d1760fd44cbd3e8cbb175de49a14fc/store_swap_ranges_exit_assigns_part3_po_why.sx)