[cfe-dev] Symbolic Extents

[Jordy Rose]

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".