> I think you at least need a formal semantics for both C

https://en.wikipedia.org/wiki/CompCert