Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Planning hierarchy
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 208
    • Issues 208
    • 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
  • #498

Closed
Open
Created May 10, 2012 by Jochen Burghardt@burghardt

Suggest to supply values of global consts to provers

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


Id Project Category View Due Date Updated
ID0001179 Frama-C Plug-in > wp public 2012-05-10 2016-06-21
Reporter Jochen Assigned To correnson Resolution fixed
Priority normal Severity tweak Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Nitrogen-20111001 Target Version - Fixed in Version Frama-C Aluminium

Description :

Wp/Simplify couldn't prove behavior-disjointness in line 5 of the attached program. The reason is that no information about the fixed values of c1 and c2 appears in the proof obligation. If the declarations in line 1-2 are replaced by #define-s, the proof is trivially found.
I suggest to replace in the proof obligation each const variable by its value, if it is known at compile time. The latter restriction is satisfied for all variables visible in contracts (as opposed e.g. to asserts). Preferring C constants to macros is considered good software engineering practice; it shouldn't be discouraged by Frama-C/Wp.

Attachments

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