Total Correctness

Should the verifier check the total correctness of a loop, sofar it has a termination clause?

If all loops in a function have _Term annotations, yes. Otherwise, no.

1 Like

It seems also that in our restrircted TinyC verification that for every statements except loops: total correctness is checked sofar the partial has been checked for them, isn’t it?

Yes, all statements except loops always terminate, so there is no need to check termination.

1 Like