diff options
| author | Guillaume Claret <dev@clarus.me> | 2015-04-02 11:27:21 +0200 |
|---|---|---|
| committer | Guillaume Claret <dev@clarus.me> | 2015-04-02 11:27:21 +0200 |
| commit | ef324b3ae2953da71efee183ba6cd2e560444688 (patch) | |
| tree | ef7cdc75108db50693686cfdf42ae5a546708d62 /README | |
| parent | 95ba79b10e832025bbc9843f9d14614f7dff0fcb (diff) | |
| download | compcert-ef324b3ae2953da71efee183ba6cd2e560444688.tar.gz compcert-ef324b3ae2953da71efee183ba6cd2e560444688.zip | |
README in MarkDown
Diffstat (limited to 'README')
| -rw-r--r-- | README | 34 |
1 files changed, 0 insertions, 34 deletions
diff --git a/README b/README deleted file mode 100644 index e9492973..00000000 --- a/README +++ /dev/null @@ -1,34 +0,0 @@ - The CompCert C verified 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 - |