Frama-C
Detailed installation instructions are available here: https://frama-c.com/html/get-frama-c.html
We advise to use the runtime assertion plugin e-acsl from the commandline. You can use the following commands to transform a file into a file with executable checks.
e-acsl-gcc.sh <file.c> -c -O <output_file>
This command generates an executable file. You can run this executable file in two different ways:
- without runtime assertion checking enabled: ./<output_file>
- with runtime assertion checking enabled: ./<output_file.e-acsl>
If you would like to inspect the checks that are inserted, you can inspect the program with run-time inserted using the GUI, with: frama-c-gui -e-acsl <file.c>.
You can use the following command to statically verify a C program with Frama-C:
- frama-c-gui -wp <file.c>
This command will open the GUI of Frama-C. If you then choose your file in the left sidebar, it will show what could (not) be verified using several icons:
- Green circle: The property and all its dependencies are valid
- Green/red circle: The property is valid but it has dependencies that have not been proven.
- Yellow circle: The property has not been validated.
- Blue outline of a circle: No proof attempted.
All of the possible icons are described in the Frama-C user manual
Links to an external site. in section 7.3 “Consolidating Property Statuses” (page 45).
Note that in the bottom window of the GUI Frama-C will show any issues that you need to be aware of, for example, if a certain annotation could not be proven because it is not supported. This will generally also give a warning about “Missing RTE guards”. This warning shows that this technique relies on the hypothesis that your program is runtime-error free. It is safe to ignore this error for now. If you are interested to try to prove the absence of runtime errors as well, then use the command: frama-c-gui -wp -wp-rte <file.c>.
OpenJML
Detailed installation instructions are available here: https://www.openjml.org/downloads/