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

[Jordy Rose]

On Sat, 5 Jun 2010 23:51:14 -0700, John McCall <rjmccall at apple.com> wrote:
> I just want to point out here that overflow is not undefined on unsigned
> integers in C, so if you're reasoning based on abstract program
semantics,
> you cannot assume unsigned overflow does not occur.  (((unsigned) x)-1
>=
> UINT_MAX) has a valid solution at x == 0U.  Signed overflow has
undefined
> behavior, so (((int) x)-1 >= INT_MAX) has no solutions given a valid
> program.
> 
> John.

Interesting, I didn't know that. I'm sure some people use the (platform
and compiler-dependent) signed wraparound too.

I guess I would want the "tautology-checking" behavior should be
enabled/disabled by a compiler flag in the long run, but for now should I
disable it, and perhaps just wait for another checker as Zhongxing said?