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

Closed
Open
Created Nov 04, 2011 by Jochen Burghardt@burghardt

suggest to provide FILE,LINE references for proof obligations in WP cmd-line output

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


Id Project Category View Due Date Updated
ID0001011 Frama-C Plug-in > wp public 2011-11-04 2011-11-04
Reporter Jochen Assigned To correnson Resolution open
Priority normal Severity feature Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Nitrogen-20111001 Target Version - Fixed in Version -

Description :

Currently, the command-line (i.e. non-gui) version of WP gives internally-generated names of proof obligations, like e.g.

[wp] [Simplify] Goal store_axiom_pop_of_push_pre31_push_stack_s1 : Valid [wp] [Simplify] Goal store_axiom_pop_of_push_pre26_pop_stack_s2 : Timeout

In order to support the user in improving his program to get it verified, it should be made clear where an unproven obligation originated from, by providing file name and line number. Although a lot of information can be found in the directory specified with "-wp-out", the FILE,LINE information cannot.

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