Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001051Frama-CPlug-in > wppublic2011-12-15 18:022011-12-16 17:34
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeveritytextReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
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? file icon store_fill_function_assigns_po_why.sx [^] (40,900 bytes) 2011-12-15 18:02
? file icon store_swap_ranges_exit_assigns_part3_po_why.sx [^] (41,644 bytes) 2011-12-16 17:26

- Relationships

-  Notes
(0002557)
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.)

- 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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker