[uecker]

Actually the definition of UB is not "compilers can assume UB does not exist" but indeed "the language spec can't guarantee anything". We clarified this in the C23 spec. (although a limited form of "compilers can assume UB does not exist" can be derived from "the spec can't guarantee anything")

[Joker_vD]

Well, I was under impression that word "anything" actually means "anything", so e.g. "the language spec can't guarantee that the compilers won't assume that the execution paths with UB on them never happen and then use that assumption for optimization" is a valid instantiation of "the language spec can't guarantee anything".

[uecker]

Actually, the spec does not say exactly "the language spec can't guarantee anything". It says "undefined behavior --- behavior, upon use of a nonportable or erroneous program construct or of erroneous data, for which this document imposes no requirements." So it says "no requirements" but this refers specifically ("for which") to the behavior in question and not the whole program. This implies that preceding observable behavior can not be affected. (but non-observable behavior can according to the "as-if" rule and this is sufficient for optimization). We added a note to clarify this in C23.