README

   1 Presentation
   2 --------------
   3
   4 This is a Frama-C plug-in and a wrapper for Lustre that makes the synthesis of
   5 the results of the CerCo compiler.
   6
   7  Requirements
   8 --------------
   9
  10   - Frama-C Nitrogen
  11   - Ocaml >= 3.12
  12   - CerCo
  13   - Lustre compiler (for Lustre files only)
  14   - Jessie plug-in and simplify (for verification only)
  15
  16  Compilation
  17 -------------
  18
  19   You can compile the plug-in and the wrapper using the following command:
  20
  21   % make
  22
  23   (assuming that you are located at the root of the source tree)
  24
  25  Installation
  26 --------------
  27
  28   You can install the plug-in and the wrapper using the following command:
  29
  30   % make install
  31
  32   You may need administrative rights.
  33
  34 Note: both the plug-in and the wrapper can be installed seperately. See their
  35 README in their respective source folders ("plugin" for the plug-in and
  36 "wrapper" for the Lustre wrapper). Also note that the wrapper uses the plug-in.
  37
  38  Usage
  39 -------
  40
  41   - Plug-in:
  42
  43     You can run the plug-in on a C file "file.c" using the following command:
  44
  45     % frama-c -cost file.c
  46
  47     The result will be in file "file-annotated.c" in the same directory if the
  48     name is fresh. Otherwise an integer suffix will be added to the base name of
  49     the output file.
  50
  51     For a complete description of the options, use the command:
  52
  53     % frama-c -cost-help
  54
  55   - Lustre wrapper:
  56
  57     You can run the wrapper for Lustre on a node "node" of a Lustre file
  58     "file.lus" using the following command:
  59
  60     % frama-c_lustre file.lus node
  61
  62     The result will be in file "file-annotated.c" in the same directory if the
  63     name is fresh. Otherwise an integer suffix will be added to the base name of
  64     the output file.
  65
  66     For a complete description of the options, use the command:
  67
  68     % frama-c_lustre -help
  69
  70   - Jessie script
  71
  72     For verification through a graphical user interface, a script that calls the
  73     Jessie plug-in of Frama-C with specific options is also provided. It can be
  74     ran using the following command on an annotated C file (obtained with the
  75     Cost plug-in for instance):
  76
  77     % frama-c_jessie annotated-file.c
  78
  79     Note: the script calls Jessie with generation of safety conditions
  80     disabled, i.e. proof obligations regarding interger overflow, pointer
  81     dereferencing, preconditions, loop variants, etc, will *not* be
  82     generated. Thus, verification with frama-c_jessie is only correct modulo
  83     safety. If you wish to turn on the generation of safety conditions you can
  84     use Jessie in its simplest form:
  85
  86     % frama-c -jessie annotated-file.c