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.