Predicate ControlFlow::mayReturnNormally

Holds if the function f may return without panicking, exiting the process, or looping forever.

This is defined conservatively, and so may also hold of a function that in fact cannot return normally, but never fails to hold of a function that can return normally.