An analysis to identify functions that never return to their caller. This only counts calls to exit, abort, or similar. Notably, exceptions are not considered since the caller can catch those.

The dataflow fact is Function does not return. It starts at False (top) and calls to termination functions move it to True. The meet operator is &&. The final result for a function is computed by meeting all of the values at the *reachable* exit instructions. If no paths can return, this will be &&(True...), which is True.