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