[cfe-commits] [patch] Tracking simple arithmetic constraints (PR2695)

[Ted Kremenek]

On Jun 10, 2010, at 12:49 AM, Zhongxing Xu wrote:

> This example gives me this idea: handling such constraints in the current Simple/Range constraint manager and SValuator framework perhaps is a mistake. To correctly handle overflow, we should have a new constraint manager, which have the full ability inside to handle various overflow conditions. 
> 
> I suggest we complete ignore overflow cases in current constraint managers. 
> 
> For the x+1>0 example, the new constraint manager should solve it according to signedness of x. If x is signed, the solution should be x \in (-1, MAX_INT], if x is unsigned, the soluction is [0, MAX_UINT]
> 
> What I mean is for constaints like x + 1 > 0, we can't use simple algebraic equality to solve it. And that complexity should be put into a new constraint manager.

I think this is reasonable.  We likely will need a new ConstraintManager entirely to handle constraints between symbolic values.  SimpleConstraintManager and its derivatives are meant to be simple, and provides a nice baseline to compare to for building smarter ConstraintManagers.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20100614/65c0a271/attachment.html>