The CompCert formally-verified C compiler
Clone or download
maximedenes and xavierleroy Use `Program Instance` instead of `Instance` + refine mode (#261)
CompCert currently uses `Instance` in so-called "refine" mode, where
Coq drops automatically in proof mode if some members of the instance
are missing.

This mode is soon going to be turned off by default, see
coq/coq#9270.

In order to make CompCert robust against this change, this commit
replaces those occurrences of `Instance` that use "refine" mode
with `Program Instance`.
Latest commit 459f641 Dec 27, 2018
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
arm Generate a nop instruction after some ais annotations (#137) Sep 12, 2018
backend Simplified code. Bug 24067 Sep 12, 2018
cfrontend Use `Program Instance` instead of `Instance` + refine mode (#261) Dec 27, 2018
common Use `Program Instance` instead of `Instance` + refine mode (#261) Dec 27, 2018
cparser Fix fixme in PackedStructs. Nov 20, 2018
debug Various improvements in the wording of diagnostics. Aug 2, 2018
doc Updates for release 3.4 Sep 17, 2018
driver Fix passing of -u to linker. Aug 21, 2018
exportclight clightgen: add info on configuration and platform to generated .v fil… Jun 20, 2018
extraction Resynchronize the LICENSE file and the license headers in individual … Jan 5, 2018
flocq flocq: minor cleaning (#257) Sep 14, 2018
lib Add functions "ordered" and "compare" to Float and Float32 Dec 20, 2018
powerpc Fix typo in asmexpand. Bug 24953 Nov 7, 2018
riscV Generate a nop instruction after some ais annotations (#137) Sep 12, 2018
runtime Define the C11 type max_align_t (#115) May 24, 2018
test Attach _Alignas to names and refactor _Alignas checks (#133) Sep 10, 2018
tools Extend the modorder tool to handle Coq files as well (#54) Feb 8, 2018
x86 x86: wrong modeling of ZF flag for FP comparisons Dec 20, 2018
x86_32 Hybrid 64bit/32bit PowerPC port May 3, 2017
x86_64 Hybrid 64bit/32bit PowerPC port May 3, 2017
.gitignore Ignore generated conflict file. Bug 24455 Sep 10, 2018
Changelog Updates for release 3.4 Sep 17, 2018
LICENSE Resynchronize the LICENSE file and the license headers in individual … Jan 5, 2018
Makefile Make generated file cparser/Parser.v read-only Aug 27, 2018
Makefile.extr Removed CMinor import. Bug 20992 Feb 14, 2017
Makefile.menhir Resynchronize the LICENSE file and the license headers in individual … Jan 5, 2018
README.md Mention the RISC-V port as well Jan 13, 2018
VERSION Update version and change log in preparation for public release 3.4 Sep 12, 2018
configure Tentatively support Coq 8.8.2 Sep 12, 2018
coq ia32/Select*: complete the modifications to shifts. Apr 11, 2014
pg ia32/Select*: complete the modifications to shifts. Apr 11, 2014

README.md

CompCert

The verified C compiler.

Overview

The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM, x86 and RISC-V 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.

For more information on CompCert (supported platforms, supported C features, installation instructions, using the compiler, etc), please refer to the Web site and especially the user's manual.

License

CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes. A commercial version of CompCert, without this restriction and with professional support, can be purchased from AbsInt. See the file LICENSE for more information.

Copyright

The CompCert verified compiler is Copyright Institut National de Recherche en Informatique et en Automatique (INRIA) and AbsInt Angewandte Informatik GmbH.

Contact

General discussions on CompCert take place on the compcert-users@inria.fr mailing list.

For inquiries on the commercial version of CompCert, please contact info@absint.com