And? Nobody expects that gcc, or intel's reference compilers, or Microsoft's compilers produce provably correct output.

How could they? The C standard contains ambiguity in several areas.