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

[Jordy Rose]

>>
>> 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.