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

[Zhongxing Xu]

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/20100611/07c9bfe7/attachment.html>