summaryrefslogtreecommitdiff
path: root/README
diff options
context:
space:
mode:
Diffstat (limited to 'README')
-rw-r--r--README57
1 files changed, 37 insertions, 20 deletions
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.