## 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.