It's the exact same analysis as ensuring all paths of a function do return the right type -- you just make sure all paths call a divergent function (typically u

It's the exact same analysis as ensuring all paths of a function do return the right type -- you just make sure all paths call a divergent function (typically unconditional panic) or enter a loop {} that never breaks/returns. This is of course a conservative analysis so e.g. "while true { }" is assumed to terminate and is rejected. Failing to perform this verification correctly would trivially lead to memory unsafety as calling code is allowed to assume such a function returns any and all requested types.