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

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

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

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

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

  You can compile the plug-in and the wrapper 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). Also 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

  - Lustre wrapper:

    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

  - Jessie script

    For verification through a graphical user interface, a script that calls the
    Jessie plug-in of Frama-C with specific options is also provided. It can be
    ran using the following command on an annotated C file (obtained with the
    Cost plug-in for instance):

    % frama-c_jessie annotated-file.c

    Note: the script calls Jessie with generation of safety conditions
    disabled, i.e. proof obligations regarding interger overflow, pointer
    dereferencing, preconditions, loop variants, etc, will *not* be
    generated. Thus, verification with frama-c_jessie is only correct modulo
    safety. If you wish to turn on the generation of safety conditions you can
    use Jessie in its simplest form:

    % frama-c -jessie annotated-file.c