[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