<div dir="ltr">Hi James, Bjarke,<br><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><br>Forgive my naivety, but wouldn't that involve solving the halting problem?<div><br></div></div></blockquote><div>Strong post-dominance does not state anything about the termination of loops. If A strongly post-dominates B, then A is executed iff B is executed. The inverse is not true, however. So if A doesn't strongly post-dominates B, A may or may not be executed after B. I.e., to prove strong post-dominance between A and B, you need to prove termination of all loops along the paths from B to A.</div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div></div></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class=""><div dir="ltr">Do we have anything in LLVM for determining strong post-dominance and in general for guaranteeing that if B is executed, then A will also be executed?<div><br></div></div></span></blockquote></div></blockquote><div>To my knowledge, this feature is currently not available.</div><div><br></div><div>Best,</div><div>Philip</div></div></div></div>