4 This is a Frama-C plug-in and a wrapper for Lustre that makes the synthesis of
5 the results of the CerCo compiler.
13 - Lustre compiler (for Lustre files only)
14 - Jessie plug-in and simplify (for verification only)
19 You can compile the plug-in and the wrapper using the following command:
23 (assuming that you are located at the root of the source tree)
28 You can install the plug-in and the wrapper using the following command:
32 You may need administrative rights.
34 Note: both the plug-in and the wrapper can be installed seperately. See their
35 README in their respective source folders ("plugin" for the plug-in and
36 "wrapper" for the Lustre wrapper). Also note that the wrapper uses the plug-in.
43 You can run the plug-in on a C file "file.c" using the following command:
45 % frama-c -cost file.c
47 The result will be in file "file-annotated.c" in the same directory if the
48 name is fresh. Otherwise an integer suffix will be added to the base name of
51 For a complete description of the options, use the command:
57 You can run the wrapper for Lustre on a node "node" of a Lustre file
58 "file.lus" using the following command:
60 % frama-c_lustre file.lus node
62 The result will be in file "file-annotated.c" in the same directory if the
63 name is fresh. Otherwise an integer suffix will be added to the base name of
66 For a complete description of the options, use the command:
68 % frama-c_lustre -help
72 For verification through a graphical user interface, a script that calls the
73 Jessie plug-in of Frama-C with specific options is also provided. It can be
74 ran using the following command on an annotated C file (obtained with the
75 Cost plug-in for instance):
77 % frama-c_jessie annotated-file.c
79 Note: the script calls Jessie with generation of safety conditions
80 disabled, i.e. proof obligations regarding interger overflow, pointer
81 dereferencing, preconditions, loop variants, etc, will *not* be
82 generated. Thus, verification with frama-c_jessie is only correct modulo
83 safety. If you wish to turn on the generation of safety conditions you can
84 use Jessie in its simplest form:
86 % frama-c -jessie annotated-file.c