Presentation
--------------

This is a wrapper of the Frama-C plug-in Cost for Lustre that makes the
synthesis of the results of the CerCo compiler on Lustre files.

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

  - Frama-C Nitrogen
  - Ocaml >= 3.12
  - Cost plug-in
  - CerCo
  - Lustre compiler
  - Jessie plug-in and simplify (for verification only)

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

  You can compile the wrapper using the following command:

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

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

  You can install the wrapper using the following command:

  % make install

  You may need administrative rights.

 Usage
-------

  You can run the wrapper for Lustre on a node "node" of a Lustre file
  "file.lus" using the following command:

  % frama-c_lustre file.lus node

  The result will be in file "file-annotated.c" in the same directory if the
  name is fresh. Otherwise an integer suffix will be added to the base name of
  the output file.

  For a complete description of the options, use the command:

  % frama-c_lustre -help