Skip to content
GitLab
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 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • 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
  • #951
Closed
Open
Issue created Nov 27, 2014 by Jochen Burghardt@burghardt

suggest to provide a command-line option for checking if every loop or recursion has a termination measuring function attached

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


Id Project Category View Due Date Updated
ID0001995 Frama-Clang Plug-in > wp public 2014-11-27 2014-11-27
Reporter Jochen Assigned To correnson Resolution open
Priority low Severity feature Reproducibility always
Platform frama-c-Neon-20140301+dev-stance OS - OS Version xubuntu-cfe13.10
Product Version - Target Version - Fixed in Version -

Description :

Section 2.5 "Termination" of the ACSL Implementation Manual says that termination can be guaranteed by attaching a termination measuring function to every loop and every recursion. In accordance with that, Frama-C doesn't complain when a loop variant is missing for some loop, and attempts to prove it if it is present.

It would be desirable to have a command-line option to let Frama-C check if every loop and every recursion has a variant/measure function attached, so a user can see whether the program can be proven to terminate - without having to check all loops and recursions (which may be tedious to detect) manually. Such an option should also be easy to implement.

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