diff options
Diffstat (limited to 'README')
| -rw-r--r-- | README | 57 |
1 files changed, 37 insertions, 20 deletions
@@ -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. |