diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-04-02 13:03:37 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-04-02 13:03:37 +0200 |
| commit | 959432fa13a899290db5236f93575a8bfdc13bb5 (patch) | |
| tree | f7a38741cb137979788352960067e847da2dc803 /README.md | |
| parent | 25d43e57763cc7d5de12a4d02d817f39a9080655 (diff) | |
| parent | 4bf7b377b16f09d133fcb4071155d6deaa976225 (diff) | |
| download | compcert-kvx-959432fa13a899290db5236f93575a8bfdc13bb5.tar.gz compcert-kvx-959432fa13a899290db5236f93575a8bfdc13bb5.zip | |
Merge branch 'master' of github.com:AbsInt/CompCert
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/README.md b/README.md new file mode 100644 index 00000000..32b419a7 --- /dev/null +++ b/README.md @@ -0,0 +1,29 @@ +# 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 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 an ongoing research project. The present release is an +advanced prototype intended for research, educational and evaluation +purposes. + +For more information on CompCert (supported platforms, supported C +features, installation instructions, using the compiler, etc), please +refer to the [user's manual](http://compcert.inria.fr/man/). + +## Copyright +The CompCert verified compiler is Copyright 2004, 2005, 2006, 2007, +2008, 2009, 2010, 2011, 2012, 2013, 2014 Institut National de Recherche en +Informatique et en Automatique (INRIA). It is distributed under the +conditions stated in file `LICENSE`. + +## Contact +The authors can be contacted by e-mail at compcert@yquem.inria.fr. |