<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><br><div><div>On Jun 29, 2010, at 1:56 PM, Jordy Rose wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><span class="Apple-style-span" style="border-collapse: separate; font-family: Helvetica; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; font-size: medium; "><br>On Tue, 29 Jun 2010 10:44:47 -0700, Ted Kremenek <<a href="mailto:kremenek@apple.com">kremenek@apple.com</a>><br>wrote:<br><blockquote type="cite">Symbol aliasing is basically alpha-renaming. We need to store on the<br></blockquote>side<br><blockquote type="cite">(within GRState) the set of alpha-renamed symbols, and when we assume<br></blockquote>that<br><blockquote type="cite">two symbols are aliased we need a callback into the Checkers so that<br></blockquote>they<br><blockquote type="cite">can decide if their current set of meta-data associated with a symbol is<br></blockquote><blockquote type="cite">compatible with assuming that two symbols are equal. The SValuator can<br></blockquote>be<br><blockquote type="cite">clever to always use an alpha-renamed symbol when building new<br></blockquote>expressions,<br><blockquote type="cite">thus folding the renaming into newly constructed SVals.<br></blockquote><br>Aliasing isn't so bad; it's the other constraints that would be harder to<br>model with sym-sym relations. But maybe we just support aliasing for a<br>while, or aliasing+linear adjustment, and ignore constraints like "a < b"<br>or "a != b".</span></blockquote></div><div><br></div><div>For "a < b" and such, isn't it a matter of unifying the constraints that already exist on 'a' and 'b'?</div><div><br></div><div><br></div></body></html>