[LLVMdev] signed/unsigned integers ?
Duncan Sands
baldrick at free.fr
Fri Apr 1 02:51:45 PDT 2011
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.
More information about the llvm-dev
mailing list