To clarify: Given a general (co)recursively enumerable problem, it's possible to come up with several semi-deciders, which won't necessarily diverge on the same

To clarify: Given a general (co)recursively enumerable problem, it's possible to come up with several semi-deciders, which won't necessarily diverge on the same inputs. So, even if I charitably interpret “undecidable program” as “program for which a static analysis tool diverges or otherwise runs into trouble”, we still need to know what specific static analysis tool we're talking about, in order to talk about what programs will be problematic for the tool. Now, I'm aware that Animats mentioned a concrete static analysis tool, the Windows Static Driver Verifier. But, without any knowledge of the specifics of how it internally works, you can't design your program to pass the verification.