[cfe-dev] Symbolic Extents
jediknil at belkadan.com
Tue Jun 29 15:56:22 CDT 2010
On Tue, 29 Jun 2010 10:44:47 -0700, Ted Kremenek <kremenek at apple.com>
> Symbol aliasing is basically alpha-renaming. We need to store on the
> (within GRState) the set of alpha-renamed symbols, and when we assume
> two symbols are aliased we need a callback into the Checkers so that
> 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
> clever to always use an alpha-renamed symbol when building new
> 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".
More information about the cfe-dev