Skip to content
GitLab
Projects Groups Topics 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
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #347
Closed
Open
Issue created Feb 24, 2017 by mantis-gitlab-migration@mantis-gitlab-migration

type of float parameter changed unexpectedly to double

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


Id Project Category View Due Date Updated
ID0002283 Frama-C Plug-in > wp public 2017-02-24 2017-05-31
Reporter widc Assigned To correnson Resolution fixed
Priority high Severity minor Reproducibility always
Platform - OS Ubuntu OS Version 16.04 LTS
Product Version Frama-C 14-Silicon Target Version - Fixed in Version Frama-C 15-Phosphorus

Description :

Current source was: sgn.c:4 The full backtrace is: Raised at file "hashtbl.ml", line 328, characters 23-32 Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38

Frama-C aborted: internal error. Your Frama-C version is Silicon-20161101.

From the floating_point.ml the following message is reported: Could not parse floating point number "-0x1.0000000000000p0"

The code in the main pane shows: float sgn(float u) ... if ((double)u > 0.0) { ...

Additional Information :

Quick solution would be appreciated.

Steps To Reproduce :

C code of sgn.c :

/*@ ensures A: \result == 1.0 || \result == 0.0 || \result == -1.0 ; / float sgn(float u)
{ float p; /
return value */ if (u > 0.0) { p = 1.0; } else if (u < 0.0) { p = -1.0; } else { p = 0.0; } return p;

}

  1. Run: frama-c-gui sgn.c
  2. Select the post-condition
  3. In context menu - Prove property by WP

(When the three "float" strings in the above code are changed to "double", the tool works fine, no error is reported.)

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