Oddities in the modeling of floats and doubles

ID0002228: This issue was created automatically from Mantis Issue 2228. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0002228	Frama-C	Plug-in > wp	public	2016-05-16	2016-05-16

Reporter	Ian	Assigned To	correnson	Resolution	open
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	Ubuntu	OS Version	-
Product Version	Frama-C Magnesium	Target Version	-	Fixed in Version	-

Description :

I a unsure of the modeling of floats and doubles provided in magnesium. There are three unexpected results I encountered.

The following program proves the contradiction with the command: frama-c -wp -wp-timeout 60 -wp-prover why3:z3-4.4.0 getNaN.c -no-tty

/*@ assigns \result; ensures \is_NaN(\result); */ extern float getNaN();

void main() { getNaN(); //@ assert Contradiction: \false; }

The following assertions are not proven (although I would expect them to be trivial) using the command: frama-c -wp -wp-timeout 60 -wp-prover alt-ergo -no-tty fin.c

void foo() { float a = 1.0; //@ assert \is_finite(a); }

void bar() { double a = 1.0; //@ assert \is_finite(a); }

The values for + or - INF are not modeled for floats or doubles. The following lemmas validate:

/*@ lemma inf_float: \forall float x; \is_finite(x) || \is_NaN(x); */

/*@ lemma inf_double: \forall double x; \is_finite(x) || \is_NaN(x); */