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