It may be interesting to look at what we have done in Ada with regard to overflow in intermediate expressions. Briefly we allow specification of three modes
all intermediate arithmetic is done in the base type, with overflow signalled if an intermediate value is outside this range. all intermediate arithmetic is done in the widest integer type, with overflow signalled if an intermediate value is outside this range. all intermediate arithmetic uses an infinite precision arithmetic package built for this purpose. In the second and third cases we do range analysis that allows smaller intermediate precision if we know it's safe. We also allow separate specification of the mode inside and outside assertions (e.g. preconditions and postconditions) since in the latter you often want to regard integers as mathematical, not subject to intermediate overflow.
