Description
-------------

  This is an experimental annotating C compiler that was built upon
  the CIL parser[1], Xavier Leroy's translation from C to Clight, and
  an existing back-end compiler for a register transfer language to a
  subset of the MIPS assembly language[2]. 

  We wrote 3 compiler passes: one from Clight to Cminor, another from
  Cminor to an abstract register transfer language (RTLabs), and a
  last one from RTLabs to an RTL that uses MIPS instructions. We
  extended interpreters for the intermediate languages to output a
  list of labels which denote key control points of the program that
  have been crossed during the interpretation. These labels are the
  places where the code can be instrumented to obtain a precise cost
  annotation. Thus, in that experiment, the annotation function is the
  composition of a labelling function followed by an instrumentation
  function.

  The architecture of the compiler is described in full details in the
  documentation of this development, which can be found in this source
  tree at doc/html/index.html.

[1] http://cil-parser.sourceforge.net/
[2] http://www.enseignement.polytechnique.fr/informatique/INF564/petit.tar.gz

 Licence
---------

  This piece of code must not be distributed. It is addressed to the
  CerCo partners only.

 Requirements
--------------

  - ocaml    (>= 3.11)
  - menhir   (>= 20090505)
  - CIL      (included in the distribution)
  - GNU Make (>= 3.8)
  - gcc

 Compilation
-------------

  You can compile this compiler using the following command:

  % make
 
  (assuming that you are located at the root of the source tree)


 Installation
--------------

  To install the compiler in your favorite system hierarchy, use:

  % PREFIX=your-directory make install

  The executable "acc" will be installed in the subdirectory "bin/" of
  "your-directory".

 Usage
-------

Usage: acc.native [options] file...
  -s              Choose the source language between:
                  Clight, Cminor
                  [default is C]
  -l              Choose the target language between:
                  Clight, Cminor, RTLabs, RTL, ERTL, LTL, LIN, ASM
                  [default is ASM]
  -i              Interpret the compiled code.
  -no-annotation  Deactivate source code annotation.
  -d              Debugging mode.
  -a              Annotate the compiled code.
  -help           Display this list of options
  --help          Display this list of options

 Test-suite
------------

  You can optionnally check that compilation went well by confronting
  the freshly built compiler to our test-suite. At the root of the
  source tree, use:

  % make check