4 This is a Frama-C plug-in that makes the synthesis of the results of the CerCo
17 You can compile the plug-in using the following command:
21 (assuming that you are located at the root of the source tree)
26 You can install the plug-in using the following command:
30 You may need administrative rights.
35 You can run the plug-in on a C file "file.c" using the following command:
37 % frama-c -cost file.c
39 The result will be in file "file-annotated.c" in the same directory if the
40 name is fresh. Otherwise an integer suffix will be added to the base name of
43 For a complete description of the options, use the command: