diff options
| -rw-r--r-- | LICENSE | 23 | ||||
| -rw-r--r-- | Makefile | 11 | ||||
| -rw-r--r-- | README | 57 |
3 files changed, 58 insertions, 33 deletions
@@ -1,7 +1,8 @@ All files in this distribution are part of the Compcert verified compiler. -The Compcert verified compiler is Copyright 2004, 2005, 2006, 2007, 2008 -Institut National de Recherche en Informatique et en Automatique (INRIA). +The Compcert verified compiler is Copyright 2004, 2005, 2006, 2007, +2008, 2009 Institut National de Recherche en Informatique et en +Automatique (INRIA). The Compcert verified compiler is distributed under the terms of the INRIA Non-Commercial License Agreement given below. This is a @@ -15,13 +16,13 @@ Foundation GNU General Public License, either version 2 or (at your option) any later version: backend/Cminor.v common/Globalenvs.v - caml/CMlexer.mli common/Mem.v - caml/CMlexer.mll common/Smallstep.v - caml/CMparser.mly common/Switch.v - caml/CMtypecheck.ml common/Values.v - caml/CMtypecheck.mli lib/Coqlib.v - caml/Cil2Csyntax.ml lib/Floats.v - caml/PrintCsyntax.ml lib/Integers.v + backend/CMlexer.mli common/Mem.v + backend/CMlexer.mll common/Smallstep.v + backend/CMparser.mly common/Switch.v + backend/CMtypecheck.ml common/Values.v + backend/CMtypecheck.mli lib/Coqlib.v + cfrontend/Cil2Csyntax.ml lib/Floats.v + cfrontend/PrintCsyntax.ml lib/Integers.v cfrontend/Csem.v lib/Maps.v cfrontend/Csyntax.v lib/Parmov.v common/AST.v runtime/calloc.c @@ -40,8 +41,8 @@ This distribution includes a copy of the CIL library and modifications to this library in the form of patches. The CIL library is Copyright 2001-2005 George C. Necula, Scott McPeak, Wes Weimer and Ben Liblit. The modifications contained in the sub-directory cil.patches/ of this -distribution are Copyright 2006, 2007 Institut National de Recherche en -Informatique et en Automatique. The CIL library and the +distribution are Copyright 2006, 2007, 2008, 2009 Institut National de +Recherche en Informatique et en Automatique. The CIL library and the modifications contained in the sub-directory cil.patches/ are distributed under the terms of the BSD license, included below. @@ -18,6 +18,7 @@ COQDOC=coqdoc OCAMLBUILD=ocamlbuild OCB_OPTIONS=\ -no-hygiene \ + -no-links \ -I extraction $(INCLUDES) \ -cflags -I,`pwd`/cil/obj/$(ARCHOS) \ -lflags -I,`pwd`/cil/obj/$(ARCHOS) \ @@ -83,10 +84,15 @@ extraction: $(MAKE) -C extraction cil: - $(MAKE) -C cil + $(MAKE) -j1 -C cil ccomp: - $(OCAMLBUILD) $(OCB_OPTIONS) Driver.native && mv Driver.native ccomp + $(OCAMLBUILD) $(OCB_OPTIONS) Driver.native \ + && rm -f ccomp && ln -s _build/driver/Driver.native ccomp + +ccomp.byte: + $(OCAMLBUILD) $(OCB_OPTIONS) Driver.byte \ + && rm -f ccomp.byte && ln -s _build/driver/Driver.byte ccomp.byte runtime: $(MAKE) -C runtime @@ -138,6 +144,7 @@ install: clean: rm -f $(patsubst %, %/*.vo, $(DIRS)) + rm -f ccomp ccomp.byte rm -rf _build rm -rf doc/html doc/*.glob rm -f doc/removeproofs.ml doc/removeproofs @@ -2,8 +2,10 @@ OVERVIEW: -The Compcert verified compiler is a compiler for a large subset of the -C programming language that generates code for the PowerPC processor. +The Compcert verified compiler is a compiler for a large subset of the +C programming language that generates code for the PowerPC and ARM +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 @@ -16,29 +18,38 @@ purposes. COPYRIGHT: -The Compcert verified compiler is Copyright 2004, 2005, 2006, 2007, 2008 -Institut National de Recherche en Informatique et en Automatique (INRIA). -It is distributed under the conditions stated in file LICENSE. +The Compcert verified compiler is Copyright 2004, 2005, 2006, 2007, +2008, 2009 Institut National de Recherche en Informatique et en +Automatique (INRIA). It is distributed under the conditions stated in +file LICENSE. -PREREQUISITES: +SUPPORTED PLATFORMS: + +- PowerPC / MacOS [stable] + For Apple Macs running the MacOS 10.4 or 10.5 operating system. + Both PowerPC-based and Intel-based Macs are supported. + The PowerPC code generated by the Compcert compiler runs + natively at full speed on PowerPC-based Macs, and runs under + software emulation at reduced speed on Intel-based Macs. -* A computer running the MacOS 10.4 or 10.5 operating system. - Both PowerPC-based and Intel-based Macs are supported. - The PowerPC code generated by the Compcert compiler runs - natively at full speed on PowerPC-based Macs, and runs under - software emulation at reduced speed on Intel-based Macs. - At least 1 Gb of RAM is required to build Compcert from sources. +- PowerPC / Linux [somewhat experimental] + For PowerPC machines running the Linux operating system. -* The XCode development tools, as found on the installation DVDs - for MacOS 10. Before proceeding, check that the "gcc", "as" and - "make" tools are installed and accessible in the search path. +- ARM / Linux [experimental] + For ARM machines running the Linux operating system. -* The Coq proof assistant, version 8.1pl3 or 8.1pl2 or 8.1. - (8.1pl1 does not work.) Coq is free software, available from - http://coq.inria.fr/ -* The Caml functional language, version 3.09 or 3.10. +PREREQUISITES: + +* The "gcc", "as" and "make" tools must be installed and accessible in + the search path. For MacOS X, you can get them by installing the + XCode development tools, as found on the installation DVDs. + +* The Coq proof assistant, version 8.1pl3. + Coq is free software, available from http://coq.inria.fr/ + +* The Caml functional language, version 3.10 or later. Caml is free software, available from http://caml.inria.fr/ @@ -46,7 +57,13 @@ INSTALLATION: 1- Configure the system. From the top directory, do: - ./configure + ./configure <target> + +where <target> is one of: + + macosx (PowerPC, MacOS X) + ppc-linux (PowerPC, Linux) + arm-linux (ARM, Linux) This generates the Makefile.config file in the top directory and prepares and configures the CIL library in the cil/ subdirectory. |