Currently, we do not check termination for loops in a function that does not itself have a termination measure. Presumably, this is because on a function call we wouldn't have a measure to compare the call with. But this is not a problem, because there cannot be a cycle of calls back to the caller (all calls in the cycle would have to have termination measures, so the call to the caller would fail).

Meanwhile, there are two very good reasons to allow termination checks in loops inside a function with out a termination measure. The minor reason is that there are many functions that have sequential that should be terminating, but also have concurrent sections for which termination cannot be proved. Second, and much more important, we need these checks to be able to safely use loops in ghost code.