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

[Jordy Rose]

SimpleSValuator already does this (and already did this before the patch).
The example was just meant to show that something may be perfectly
reasonable code, but we can't always make assumptions that seem obvious.
(Example: x+1 < 5 does not imply that x < 5.) This is of course part of
what it means to correctly model overflow. I just used "length" in the
example to show how it might look like in code.


On Mon, 14 Jun 2010 17:52:01 -0700, Ted Kremenek <kremenek at apple.com>
wrote:
> Just catching up on this thread.  Doing a substitution of of symbols
> constrained to be a constant would be useful, but really is just a
special
> case.  Handling the relationship between two symbols would result in the
> cross-product of their domains (which in the case of
> RangeConstraintManager, is the cross-product of their ranges).
> 
> On Jun 10, 2010, at 5:06 PM, Zhongxing Xu wrote:
> 
>> If length is fixed to a constant by a previous constraint or is a
>> constant, then what is the difference between
>> 
>> x + a < b  and x + 1 < length ? 
>> 
>> I think they are the same and can be solved by your algorithm, except
>> that if length is constrained to a constant we need an extra step to
>> replace the constant in.