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); */