[ummonk]

The C standard changed its note about "permissible" undefined behavior (in C89/90) to "possible" undefined behavior (from C99 onwards). This is easily verifiable and not a myth.

As to CompCert, I'm not sure if they still make guarantees about type punning, but the older paper had said this:

"The semantics of Clight is formally defined in big-step operational style. The semantics is deterministic and makes precise a number of behaviors left unspecified or undefined in the ISO C standard, such as the sizes of data types, the results of signed arithmetic operations in case of overflow, and the evaluation order. Other undefined C behaviors are consistently turned into “going wrong” behaviors, such as dereferencing the null pointer or accessing arrays out of bounds. Memory is modeled as a collection of disjoint blocks, each block being accessed through byte offsets; pointer values are pairs of a block identifier and a byte offset. This way, pointer arithmetic is modeled accurately, even in the presence of casts between incompatible pointer types"