Frama-C Bug Tracking System - Frama-C
View Issue Details
0002228Frama-CPlug-in > wppublic2016-05-16 16:422016-05-16 16:42
Frama-C Magnesium 
0002228: Oddities in the modeling of floats and doubles
I a unsure of the modeling of floats and doubles provided in magnesium. There are three unexpected results I encountered. 1. 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; } 2. 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); } 3. 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); */
No tags attached.
Issue History
2016-05-16 16:42IanNew Issue
2016-05-16 16:42IanStatusnew => assigned
2016-05-16 16:42IanAssigned To => correnson

There are no notes attached to this issue.