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
  • #351

Closed
Open
Created May 10, 2017 by mantis-gitlab-migration@mantis-gitlab-migration

Some ACSL mathematical functions crash WP

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


Id Project Category View Due Date Updated
ID0002299 Frama-C Plug-in > wp public 2017-05-10 2017-05-10
Reporter boyer Assigned To correnson Resolution open
Priority high Severity block Reproducibility always
Platform VirtualBox (Host Win7) OS Ubuntu OS Version 16.04.2
Product Version Frama-C 14-Silicon Target Version - Fixed in Version -

Description :

Some of the mathematical functions enumerated in http://frama-c.com/download/acsl.pdf, p24 are not correctly supported by Frama-c. For instance, the keywords \pow, \cos and \sin are recognized at parsing and supported by EVA whereas an error is reported for WP (builtin functions are not defined) followed by an internal error.

Additional Information :

Console message:

[kernel] Parsing .opam/4.04.0/share/frama-c/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing ex.c (with preprocessing) [wp] Running WP plugin... [wp] warning: Missing RTE guards [wp] user error: Builtin \round_error(float32) not defined [wp] failure: Logic '\round_error' undefined

Crash report:

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

Plug-in wp aborted: internal error. Reverting to previous state. [...]

Steps To Reproduce :

Using Example 2.9, p25 from the ACSL manual: /@ requires \abs(\exact(x)) <= 0x1p-5; @ requires \round_error(x) <= 0x1p-20; @ ensures \abs(\exact(\result)-\cos(\exact(x))) <= 0x1p-24; @ ensures \round_error(\result) <= \round_error(x) + 0x3p-24; @/ float cosine(float x) { return 1.0f - x * x * 0.5f; } Then: frama-c-gui -wp cosine.c

Attachments

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