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.
|Plug-in > wp
|Fixed in Version
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.