Mechanized semantics for the Clight subset of the C language

Sandrine Blazy, Xavier Leroy

This article presents the formal semantics of a large subset of the C language called Clight. Clight includes pointer arithmetic, "struct" and "union" types, C loops and structured…