Today most computing is done on two’s complement machines with integer operands with a number of bits which is a power of two. There are many convenient and efficient computing tricks you can with this knowledge. Many of these tricks result in programs to which the official definition of C ascribes no ‘stable’ meaning and leaves the implementation to do what ever is easy and presumably fast. Recent compilers omitted some unstable safety checks because the language specs do not define their meaning. Safety was silently lost. This note proposes some additional constraints on C to make some of these familiar tricks official in a language I call Super C here. Every program in C without unstable constructs is a correct program in Super C with the same meaning. I imagine yet another language option on the command line. I do not propose to remove all ambiguity. A range of such languages might be defined but I do not explore that here. Similar extensions of languages might be possible.

Quote from xx,section 3.4.3: undefined behavior

I propose a set of axioms which are to always hold. The expression prefix “All x” is to assert that the following expression always yields 1, which means “true” in C.

Modulo Arithmetic

When C was invented not all computers had adopted two’s complement arithmetic. Each of the following axioms is to hold when the x, y and z are the
All x (All y (All z (x+(y+z) == (x+y)+z)))
This did not generally hold for sign and magnitude machines.
(x is unsigned and All x ((x+1 > x) || (x+1 == 0)))
  or x is signed and All x ((x+1 > x) || (x+1 == -1)))