summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--LICENSE23
-rw-r--r--Makefile11
-rw-r--r--README57
3 files changed, 58 insertions, 33 deletions
diff --git a/LICENSE b/LICENSE
index 6a686e5..3626820 100644
--- a/LICENSE
+++ b/LICENSE
@@ -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.
diff --git a/Makefile b/Makefile
index 7c92a33..01bb8be 100644
--- a/Makefile
+++ b/Makefile
@@ -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
diff --git a/README b/README
index 9cfad16..afb358d 100644
--- a/README
+++ b/README
@@ -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.