wrapper/README

   1 Presentation
   2 --------------
   3
   4 This is a wrapper of the Frama-C plug-in Cost for Lustre that makes the
   5 synthesis of the results of the CerCo compiler on Lustre files.
   6
   7  Requirements
   8 --------------
   9
  10   - Frama-C Nitrogen
  11   - Ocaml >= 3.12
  12   - Cost plug-in
  13   - CerCo
  14   - Lustre compiler
  15   - Jessie plug-in and simplify (for verification only)
  16
  17  Compilation
  18 -------------
  19
  20   You can compile the wrapper using the following command:
  21
  22   % make
  23
  24   (assuming that you are located at the root of the source tree)
  25
  26  Installation
  27 --------------
  28
  29   You can install the wrapper using the following command:
  30
  31   % make install
  32
  33   You may need administrative rights.
  34
  35  Usage
  36 -------
  37
  38   You can run the wrapper for Lustre on a node "node" of a Lustre file
  39   "file.lus" using the following command:
  40
  41   % frama-c_lustre file.lus node
  42
  43   The result will be in file "file-annotated.c" in the same directory if the
  44   name is fresh. Otherwise an integer suffix will be added to the base name of
  45   the output file.
  46
  47   For a complete description of the options, use the command:
  48
  49   % frama-c_lustre -help