4 This is a wrapper of the Frama-C plug-in Cost for Lustre that makes the
5 synthesis of the results of the CerCo compiler on Lustre files.
15 - Jessie plug-in and simplify (for verification only)
20 You can compile the wrapper using the following command:
24 (assuming that you are located at the root of the source tree)
29 You can install the wrapper using the following command:
33 You may need administrative rights.
38 You can run the wrapper for Lustre on a node "node" of a Lustre file
39 "file.lus" using the following command:
41 % frama-c_lustre file.lus node
43 The result will be in file "file-annotated.c" in the same directory if the
44 name is fresh. Otherwise an integer suffix will be added to the base name of
47 For a complete description of the options, use the command:
49 % frama-c_lustre -help