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 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • 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
  • #2346
Closed
Open
Issue created Oct 12, 2010 by Jochen Burghardt@burghardt

Suggest to close a section if each obligation is proven by *some* prover

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


Id Project Category View Due Date Updated
ID0000602 Frama-C Graphical User Interface public 2010-10-12 2010-10-13
Reporter Jochen Assigned To monate Resolution not fixable
Priority normal Severity feature Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Boron-20100401 Target Version - Fixed in Version -

Description :

Currently, a section (like e.g. "fctxxx default behaviour" is automatically closed when one prover was able to prove all its contained obligations. However, often no single prover can prove them all, but each of them can be proved by some prover (i.e. in each line a green bullet appears, although not in the same column).

As a result, the user has to check all lines by himself, which is tedious (and even error-prone) when sections are large and the process of finding an adequate and verifiable specification involves many edit->vcg->prove cycles.

Therefor, I suggest to close a section once the statistics count has reached 100% of proven obligations (i.e. n/n). A "summary column" could be introduced showing a green bullet for single a obligation if it was proven by some prover, and a green check-mark for a section if its statistics count is 100%. For "very large" programs, it might even be desirable to have an icon summarizing all sections, i.e. the whole program, in a corresponding way.

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