diff options
Diffstat (limited to 'README')
| -rw-r--r-- | README | 144 |
1 files changed, 144 insertions, 0 deletions
@@ -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 + |