Clight

Clight is a fairly large subset of the C programming language. It is the language that is compiled by the CompCert compiler. As such, it comes with a precise formal semantics.

See also

CompCert
C

References

The formal semantics of Clight are given in

Blazy, S., Leroy, X. Mechanized Semantics for the Clight Subset of the C Language. Journal of Automated Reasoning 43, 263–288 (2009). https://doi.org/10.1007/s10817-009-9148-3 arXiv pdf