summaryrefslogtreecommitdiff
path: root/README
diff options
context:
space:
mode:
Diffstat (limited to 'README')
-rw-r--r--README144
1 files changed, 144 insertions, 0 deletions
diff --git a/README b/README
new file mode 100644
index 0000000..9cfad16
--- /dev/null
+++ b/README
@@ -0,0 +1,144 @@
+ The Compcert verified compiler
+
+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 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.
+
+
+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.
+
+
+PREREQUISITES:
+
+* 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.
+
+* 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.
+
+* 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.
+ Caml is free software, available from http://caml.inria.fr/
+
+
+INSTALLATION:
+
+1- Configure the system. From the top directory, do:
+
+ ./configure
+
+This generates the Makefile.config file in the top directory
+and prepares and configures the CIL library in the cil/ subdirectory.
+
+The "configure" script accepts the following options:
+
+-bindir <dir> (default: /usr/local/bin)
+ Directory where the binaries will be installed
+
+-libdir <dir> (default: /usr/local/lib/compcert)
+ Directory where the Compcert support library will be installed
+
+-prefix <dir> (default: /usr/local)
+ Set bindir and libdir to
+ <dir>/bin and <dir>/lib/compcert, respectively.
+
+2- Build the system. From the top directory, do
+
+ make all
+
+This re-checks all the Coq proofs, then extracts Caml code from the
+Coq specification and combines it with the CIL library and supporting
+hand-written Caml code to generate the executable for Compcert. This
+step takes 10 to 15 minutes on a recent Mac computer; be patient.
+
+3- You can now install Compcert. This will create the "ccomp" command
+in the binary directory selected during configuration, and install
+supporting .h and .a files in the library directory. Become superuser
+if necessary and do
+
+ make install
+
+
+USAGE:
+
+The executable for Compcert is called "ccomp". It has the standard
+command-line interface for a Unix C compiler. For instance, to
+compile the single-file program "src.c" and create an executable
+called "exec", just do
+
+ ccomp -o exec src.c
+
+To compile a two-file program "src1.c" and "src2.c", do
+
+ ccomp -c src1.c
+ ccomp -c src2.c
+ ccomp -o exec src1.o src2.o
+
+To see the generated assembly code for "src1.c", do
+
+ ccomp -S src1.c
+
+The generated assembly code is left in file src1.s
+
+The subset of the C language accepted by Compcert is quite large.
+The main features of C that are not supported are:
+ - The "long long" and "long double" types.
+ - The "goto" statement, and non-structured forms of the "switch" statement.
+ - Variable-argument functions.
+The "ccomp" command will issue errors and diagnostics if it encounters
+a C construct that it cannot process.
+
+The "ccomp" command recognizes the following classes of input files:
+ .c C source file
+ .cm Cminor source file
+ .o Object code file
+ .a Library file
+
+The "ccomp" command recognizes the following options:
+
+Processing options:
+ -E Preprocess only, save result in <file>.i
+ -S Compile to assembler only, save result in <file>.s
+ -c Compile to object file only (no linking), result in <file>.o
+Preprocessing options:
+ -I<dir> Add <dir> to search path for #include files
+ -D<symb>=<val> Define preprocessor symbol
+ -U<symb> Undefine preprocessor symbol
+Compilation options:
+ -flonglong Treat 'long long' as 'long' and 'long double' as 'double'
+ -dclight Save generated Clight in <file>.light.c
+ -dasm Save generated assembly in <file>.s
+Linking options:
+ -l<lib> Link library <lib>
+ -L<dir> Add <dir> to search path for libraries
+ -o <file> Generate executable in <file> (default: a.out)
+General options:
+ -stdlib <dir> Set the path of the Compcert run-time library
+ -v Print external commands before invoking them
+
+
+CONTACT:
+
+The authors can be contacted by e-mail at compcert@yquem.inria.fr
+