[PATCH] D12901: [Static Analyzer] Intersecting ranges and 64 bit to 32 bit truncations causing "System is over constrained." assertions.

[pierre gousseau via cfe-commits]

pgousseau added a comment.

In http://reviews.llvm.org/D12901#248842, @xazax.hun wrote:

> Hi!
>
> Thank you for the patch!


Thanks for reviewing !

> What happens if you factor the "index + 1" expression out into a separate variable?

>  E.g.: unsigned temp = index + 1; and use temp in the condition?


In this case the symbol 'temp' is still considered by the analyzer as a 'Sym + Int' symbol so the same code path is followed.
I will add the test case thanks !

> My impression is that, the ranges does not model the overflow behavior correctly (which is well defined for unsigned values). I wondering why do you think that, the right way to solve this is to modify assumeSymNE and assumeSymEQ? Wouldn't it be better to actually handle the ranges properly on assignments and other operations (such as +), so assumeSymNE and assumeSymEQ can remain unmodified?


Yes handling ranges properly would be better! I am trying to fix the assertion without having to do too much re-engineering, I agree that changing assumeSymNE/assumeSymEQ's interfaces is not ideal but it has I hope the advantage of making the purpose of the change clearer and easier to revert should modelling of truncations/promotions be added ? Any ideas on how I could avoid changing the interface?

Regards,

Pierre


http://reviews.llvm.org/D12901