Compcert C Compiler
High-assurance compiler for almost all of the C language (ISO C99), generating efficient code for the PowerPC, ARM, RISC-V and x86 processors.
similar
-
CertiCoq github.com
Verified compiler from Gallina, the internal language of Coq, down to CompCert's Clight language.
-
-
SmallerC github.com
Portable self-hosting C compiler capable of producing executables for a number of platforms, including real and protected mode DOS programs, by Alexei A. Frounze.
-
-
scc github.com
Sloc Cloc and Code, a very fast accurate code counter with complexity calculations and COCOMO estimates.
-
OCaml › Compilers and Compiler Tools: “It is a C Compiler supporting most of the ISO C90 and C99 / ANSI C features.”
Coq › Projects > Verified Software: “High-assurance compiler for almost all of the C language (ISO C99), generating efficient code for the PowerPC, ARM, RISC-V and x86 processors.”