[LLVMdev] signed/unsigned integers ?

[Duncan Sands]

Hi Julian,

> Suppose I approximate the set of possible values for my variable "x" with
> intervals.
> I think there are some cases for which I'll be unable to find precise enough
> invariants, for example, I'd like this:
>
> unsigned x;
> // x >= 0
> if (x != 0) {
> // x >= 1
> ...
> }
>
> but since I consider x in ]-oo; +oo[, I have this:
>
> unsigned x;
> // x in ]-oo; +oo[
> if (x != 0) {
> // x in ]-oo; +oo[ (because of the abstraction by intervals)
> ...
> }

in fact there is no problem here, because "x >= 1" becomes an unsigned uge
comparison in LLVM.  The values for which "x uge 1" are true are
]-oo; -1], [1, +oo[ (this range is an interval if you allow intervals to
wrap around the end), so you can deduce that "x uge 1" is true from x != 0.

Ciao, Duncan.