Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002228Frama-CPlug-in > wppublic2016-05-16 16:422016-05-16 16:42
ReporterIan 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSUbuntuOS Version
Product VersionFrama-C Magnesium 
Target VersionFixed in Version 
Summary0002228: Oddities in the modeling of floats and doubles
DescriptionI 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);
*/
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2016-05-16 16:42 Ian New Issue
2016-05-16 16:42 Ian Status new => assigned
2016-05-16 16:42 Ian Assigned To => correnson


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker