Ajout license, README, copyright notices

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

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
+