> Hmm, won't (uint32_t + uint32_t-CST) doesn't overflow be sufficient > condition for such transformation?
Yes, in principle this should suffice. What we're actually looking for is something like a "proper" (or no) overflow, i.e. an overflow in both min and max of the value range. In (a + cst1) + cst2 an overflow of (a + cst1) will still produce a valid range as long as overflow(a_min + cst1) == overflow(a_max + cst1). When max overflows but min does not we must not simplify. Currently, I'm checking if the range of (a + cst1) is still a VR_RANGE, for now disregarding ANTI_RANGEs which could most likely be dealt with as well. A major discussion point in my last try was to wrongly always use sign-extend when extending cst1 to the outer type. This is now changed to use sign-extension when (a + cst1) "properly" overflows as in ASSUME (a > 0); (unsigned long)(a + UINT_MAX) + 1; resulting in (unsigned long)(a) + (unsigned long)0, or use the type sign of the constant like in ASSUME (a < 2); (unsigned long)(a + 4294967294u) + 10; resulting in (unsigned long)(a) + (unsigned long)((unsigned long)4294967294 + (unsigned long)10). The additional flag from the last patch is not necessary. Test suite is clean on s390x and x86, bootstraps successful. Regards Robin