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
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 208
    • Issues 208
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • 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
  • #334

Closed
Open
Created Jun 15, 2017 by Jochen Burghardt@burghardt

poor errors message texts for Hoare memory model checks

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


Id Project Category View Due Date Updated
ID0002311 Frama-C Plug-in > wp public 2017-06-15 2017-06-15
Reporter Jochen Assigned To correnson Resolution open
Priority normal Severity text Reproducibility sometimes
Platform Phosphorus-20170501-beta1 OS xubuntu OS Version -
Product Version Frama-C 15-Phosphorus Target Version - Fixed in Version -

Description :

Running "frama-c -wp -wp-rte -wp-model Hoare memmodel_Hoare.c" on the attached program produces the output:

... [rte] annotating function foo memmodel_Hoare.c:5:[wp] warning: Can not load value in Empty model memmodel_Hoare.c:5:[wp] warning: Can not load value in Empty model memmodel_Hoare.c:8:[wp] warning: Can not load value in Empty model memmodel_Hoare.c:8:[wp] warning: No validity memmodel_Hoare.c:4:[wp] warning: Can not load value in Empty model memmodel_Hoare.c:3:[wp] warning: No validity [wp] 4 goals scheduled ...

The name of the memory model is "Hoare" on the command line and in the WP manual (Sect.3.2, p.44), but it is called "Empty" in the error message output. Moreover, the message "No validity" should be expanded to be more understandable. As an additional convenience, Frama-C could mention in each message the variable it refers to ("x" resp. "*x") in all cases in the example).

Attachments

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