source: Deliverables/D5.1/frama-c-cost-plugin/Nitrogen/README @ 2749

Last change on this file since 2749 was 2749, checked in by regisgia, 8 years ago
  • Updated version of the Frama-C plugin.
File size: 2.5 KB
Line 
1Presentation
2--------------
3
4This is a Frama-C plug-in and a wrapper for Lustre that makes the synthesis of
5the 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
34Note: both the plug-in and the wrapper can be installed seperately. See their
35README 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
Note: See TracBrowser for help on using the repository browser.