source: Deliverables/D5.1-5.3/cost-plug-in-indexed-labels-branch/README

Last change on this file was 1689, checked in by tranquil, 8 years ago

kept out the wrapper (which I did not touch, so not sure it works)

File size: 1.2 KB
Line 
1Presentation
2--------------
3
4This is a Frama-C plug-in that makes the synthesis of the results of the CerCo
5compiler, using its indexed labels features.
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 and the wrapper using the following command:
26
27  % make install
28
29  You may need administrative rights.
30
31Note: both the plug-in and the wrapper can be installed seperately. See their
32README in their respective source folders ("plugin" for the plug-in and
33"wrapper" for the Lustre wrapper). Note that the wrapper uses the plug-in.
34
35 Usage
36-------
37
38  - Plug-in:
39
40    You can run the plug-in on a C file "file.c" using the following command:
41
42    % frama-c -cost file.c
43
44    The result will be in file "file-annotated.c" in the same directory if the
45    name is fresh. Otherwise an integer suffix will be added to the base name of
46    the output file.
47
48    For a complete description of the options, use the command:
49
50    % frama-c -cost-help
51
Note: See TracBrowser for help on using the repository browser.