[cfe-dev] Symbolic Extents

[Ted Kremenek]

On Jun 29, 2010, at 1:56 PM, Jordy Rose wrote:

> 
> On Tue, 29 Jun 2010 10:44:47 -0700, Ted Kremenek <kremenek at apple.com>
> wrote:
>> Symbol aliasing is basically alpha-renaming.  We need to store on the
> side
>> (within GRState) the set of alpha-renamed symbols, and when we assume
> that
>> two symbols are aliased we need a callback into the Checkers so that
> they
>> can decide if their current set of meta-data associated with a symbol is
>> compatible with assuming that two symbols are equal.  The SValuator can
> be
>> clever to always use an alpha-renamed symbol when building new
> expressions,
>> thus folding the renaming into newly constructed SVals.
> 
> Aliasing isn't so bad; it's the other constraints that would be harder to
> model with sym-sym relations. But maybe we just support aliasing for a
> while, or aliasing+linear adjustment, and ignore constraints like "a < b"
> or "a != b".


For "a < b" and such, isn't it a matter of unifying the constraints that already exist on 'a' and 'b'?


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20100629/4244090e/attachment.html>