The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM and x86 processors. The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code. CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes.
3 lines
113 B
Plaintext
3 lines
113 B
Plaintext
SHA256 (CompCert-2.5.tar.gz) = NoR7APpUNqyOBSSJtyit7yvGgGT+ItvcGL8iJWhW/ZU=
|
|
SIZE (CompCert-2.5.tar.gz) = 2340145
|