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