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.
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]