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

[Ted Kremenek]

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.
> 
> On Fri, Jun 11, 2010 at 2:30 AM, Jordy Rose <jediknil at belkadan.com> wrote:
> 
> >>
> >> This, while long and not particularly friendly or derivable (I had
> >> several
> >> false starts), is not too hard to code, and seems to be working! And
> more
> >> importantly, it's correctly modeling C behavior. I'll get it done soon.
> >>
> >> The downside, as you point out, is that it can't actually do much with:
> >>
> >> if (x+1 < length) {
> >>  // do something relying on x being small
> >> }
> >>
> >> ...since x could be (U)INT_MAX here.
> >>
> >
> > Do you mean 'x' and 'length' are both symbolic here? We can give up for
> > such
> > cases for now.
> 
> Oh, no, I meant in cases where "length" was fixed by a previous branch. Or
> just a constant, I suppose.
> 
> I am hoping to have symbolic relations by the end of the summer though (at
> least additive ones), as part of my GSoC project. One step at a time,
> though.
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20100614/e23db66d/attachment.html>