Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #509

Closed
Open
Created May 16, 2016 by mantis-gitlab-migration@mantis-gitlab-migration

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

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking