Enforce loop termination checking

[hanno-becker]

In mlkem-native and mldsa-native, we would like to be able to claim that we check termination of loops except for a small number of loops which only probabilistically terminate. Of course, we can point at the individual decreases clauses and ask a consumer to grep-validate our claims, but this is inconvenient.

Could CBMC offer a flag which, if set, makes CBMC fail upon encountering a loop for which no termination argument is given (or can be synthesized, if this is something that CBMC does in places)?

[kroening]

This is on by default, just try CBMC on a few loops without any command line arguments.

You'll see properties like this:

[main.unwind.0] line 6 unwinding assertion loop 0: FAILURE

[hanno-becker]

This is for loops that are unwound, though, isn't it? What about loops specified by invariant?

[kroening]

Ah, yes, such a flag can be added.