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.