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

This is a Frama-C plug-in that makes the synthesis of the results of the CerCo
compiler, using its indexed labels features.

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

  - Frama-C Carbon
  - CerCo

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

  You can compile the plug-in using the following command:

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

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

  You can install the plug-in and the wrapper using the following command:

  % make install

  You may need administrative rights.

Note: both the plug-in and the wrapper can be installed seperately. See their
README in their respective source folders ("plugin" for the plug-in and
"wrapper" for the Lustre wrapper). Note that the wrapper uses the plug-in.

 Usage
-------

  - Plug-in:

    You can run the plug-in on a C file "file.c" using the following command:

    % frama-c -cost file.c

    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 -cost-help