You're using the Turing Tarpit here. You do not need to "solve the Halting Problem" in order to make useful static analysis software. When the software can pro

You're using the Turing Tarpit here. You do not need to "solve the Halting Problem" in order to make useful static analysis software. When the software can prove X, return True. When the software can prove !X, return False. When the software can't do either, return Sorry.