plugin/README

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