source: Deliverables/D5.1/cost-plug-in/README @ 1462

Last change on this file since 1462 was 1462, checked in by ayache, 8 years ago

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File size: 1.7 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 Carbon
11  - CerCo
12  - Lustre compiler (for Lustre files only)
13  - Jessie plug-in and simplify (for verification of Lustre files only)
14
15 Compilation
16-------------
17
18  You can compile the plug-in and the wrapper using the following command:
19
20  % make
21 
22  (assuming that you are located at the root of the source tree)
23
24 Installation
25--------------
26
27  You can install the plug-in and the wrapper using the following command:
28
29  % make install
30
31  You may need administrative rights.
32
33Note: both the plug-in and the wrapper can be installed seperately. See their
34README in their respective source folders ("plugin" for the plug-in and
35"wrapper" for the Lustre wrapper). Note that the wrapper uses the plug-in.
36
37 Usage
38-------
39
40  - Plug-in:
41
42    You can run the plug-in on a C file "file.c" using the following command:
43
44    % frama-c -cost file.c
45
46    The result will be in file "file-annotated.c" in the same directory if the
47    name is fresh. Otherwise an integer suffix will be added to the base name of
48    the output file.
49
50    For a complete description of the options, use the command:
51
52    % frama-c -cost-help
53
54  - Lustre wrapper:
55
56    You can run the wrapper for Lustre on a node "node" of a Lustre file
57    "file.lus" using the following command:
58
59    % frama-c_lustre file.lus node
60
61    The result will be in file "file-annotated.c" in the same directory if the
62    name is fresh. Otherwise an integer suffix will be added to the base name of
63    the output file.
64
65    For a complete description of the options, use the command:
66
67    % frama-c_lustre -help
Note: See TracBrowser for help on using the repository browser.