[cfe-dev] Symbolic Extents
Ted Kremenek
kremenek at apple.com
Tue Jun 29 17:59:22 PDT 2010
On Jun 29, 2010, at 5:52 PM, Jordy Rose wrote:
> Something like that, but fully modeling it can get complicated very
> quickly:
>
> a < b
> a < c
> // a != MAX, but other than that we know nothing
> b == 11
> // at this point a < 11
> c == 10
> // now a < 10
>
> In the long-term I think we're going to want to arbitrarily impose an
> order on symbols, so that higher symbols depend on lower ones and not the
> other way around.
An ordering like this is essentially what is done in the Archer paper:
http://portal.acm.org/citation.cfm?id=940115
(PDF: http://theory.stanford.edu/~yxie/archer.pdf)
> Alternately (or additionally?), we could have a
> notification system of some kind: when a min or max value changes, ping any
> dependent symbols.
Yes this is basically a gradually relaxation of the constraints.
>
> Constraints can form arbitrarily complex graphs, in theory, and we do have
> to limit that.
Absolutely. What constraints can be handled should be dictated by the ConstraintManager.
> Unifying the current constraints is certainly an improvement
> over our current state.
More information about the cfe-dev
mailing list