> the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code that suggests to me you could still hit C's

> the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code that suggests to me you could still hit C's undefined behaviors. It's only guaranteeing the semantic equivalence between source and output