deficient axioms
ID0002138: This issue was created automatically from Mantis Issue 2138. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002138 | Frama-C | Plug-in > wp | public | 2015-06-29 | 2015-06-29 |
| Reporter | DavidCok | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | Windows | OS Version | 7 |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
The proof of the following with -WP and alt-ergo fails:
/*@ requires (int)(x+y) == x+y; ensures \result == x+y; */ int f(int x, int y) { return x+y; }
On inspecting the intermediate artifacts, we identified the problem as inadequate axioms. Two solutions requiring changes in axioms worked for us. However, I don't know if either change would have wider ramifications.
axiom is_to_sint32 : (forall x:int [is_sint32(to_sint32(x))]. is_sint32(to_sint32(x)))
The effect of the triggers in this axiom is simply to allow is_sint32(to_sint32(x)) to be reduced to true. In fact the more common need is to know that to_sint32(x) satisfies is_sint32. The proof above goes through if the trigger is changed to
axiom is_to_sint32 : (forall x:int [to_sint32(x)]. is_sint32(to_sint32(x)))
axiom id_sint32 : (forall x:int [to_sint32(x)]. ((((-2147483648) <= x) and (x < 2147483648)) -> (to_sint32(x) = x)))
This axiom is much more useful if it is written as an equivalence instead of an implication. Doing so also enables the proof of the program above to go through.