source: Deliverables/D5.1/cost-plug-in/wrapper/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.0 KB
Line 
1Presentation
2--------------
3
4This is a wrapper of the Frama-C plug-in Cost for Lustre that makes the
5synthesis of the results of the CerCo compiler on Lustre files.
6
7 Requirements
8--------------
9
10  - Frama-C Carbon
11  - Cost plug-in
12  - CerCo
13  - Lustre compiler
14  - Jessie plug-in and simplify (for verification only)
15
16 Compilation
17-------------
18
19  You can compile 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 wrapper using the following command:
29
30  % make install
31
32  You may need administrative rights.
33
34 Usage
35-------
36
37  You can run the wrapper for Lustre on a node "node" of a Lustre file
38  "file.lus" using the following command:
39
40  % frama-c_lustre file.lus node
41
42  The result will be in file "file-annotated.c" in the same directory if the
43  name is fresh. Otherwise an integer suffix will be added to the base name of
44  the output file.
45
46  For a complete description of the options, use the command:
47
48  % frama-c_lustre -help
Note: See TracBrowser for help on using the repository browser.