Comment by aeneasmackenzie

Compcert guarantees that the executable that comes out does what the code that went in said, it doesn’t guarantee much about the code that went in.