<div dir="ltr"><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><div class="h5"><br>
><br>
> You need to distinguish between not visited and visited but undef.<br>
<br>
</div></div>What I'm getting at is, if you're implementing something close to the<br>
paper mentioned, I can't think of a case where you'd care to<br>
distinguish between "not visited" and "visited but undef".  That is,<br>
instead of starting from "map each each instruction as not visited" we<br>
should be able to (my unproven conjecture) start from "map each<br>
instruction to undef", making the "unknown" element superfluous.<br></blockquote><div><br></div><div>See the email i just sent. </div><div><br></div><div>Your scheme would work if you didn't want to optimize undef, because you'd just make meet (anything, undef) -> overdefined.</div><div>It's the "we want to fill in values for undef" that makes it so you need to know when you can actually do that.</div><div>(and as mentioned, you don't need a separate post-resolver to do *what we do now*, and so far, it has just been a source of bugs :()</div><div><br></div></div></div></div>