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.
_______________________________________________
cfe-commits mailing list
cfe-commits@cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
