Commit 46629814 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Update README

parent 59aaa4f1
# MAIN README
Frama-C Verification of Paparazzi
=================================
This GitLab project is a fork of Paparazzi UAV autopilot
......@@ -15,7 +13,7 @@ Required software
-----------------
To run the verification, the following software are required:
- Frama-C, the compiled version from the
- Frama-C, the compiled version from the
[source](https://git.frama-c.com/pub/frama-c), tested on commit:
3fa7de0c695188a9b0adf7a8b8bfb24a335c1df7
- Alt-Ergo 2.3.3
......@@ -23,6 +21,11 @@ To run the verification, the following software are required:
- Z3 4.8.6
- ctags
**Note:** This specific version of Frama-C is needed because it
fixes a bug that prevented proving some goals. Also, the
_statement contracts_ are used in the proofs, but this feature
has been removed in newer versions.
How to run the verification:
-------------
```
......@@ -38,7 +41,7 @@ launch the script that start the analysis:
```
Quick descritpion of modified files:
----------------------------------------
------------------------------------
- `sw/airborne/frama-c-analysis.sh`: Script to automatically
launch the verification using Frama-C.
......@@ -56,19 +59,34 @@ Definition of predicates, lemma and logical functions for the
verification of functional properties.
The verification:
-------------
-----------------
The Frama-C verification combines the analysis of the [EVA]
(https://frama-c.com/fc-plugins/eva.html) and
[WP](https://frama-c.com/fc-plugins/wp.html) plugins. The
plugin EVA requires a program entry point (a
main or a function) to start its analysis. The script
`frama-c-analysis.sh` find automatically all the function's
name of the library using ctags. Then, the verification is
launched for every function.
name of the library using ctags. Then, the Frama-C verification is
launched for every function `FUNCTION` with the following
parameters:
When Frama-C is launched, the C constant `FRAMA_C_ANALYSIS` is
defined in order to remove certain portions of code that are not
supported by Frama-C.
- `-rte`: Add RTE annotations in the code.
- `-no-warn-left-shift-negative`: Allow left shift for negative values.
- `-eva -lib-entry -main $FUNCTION`: Launch EVA analysis with
`$FUNCTION` as the entry point. The initial state is determined by
the _preconditions_ in the contract of the function.
- `-wp-fct $FUNCTION`: Launch the WP verification with the options:
- `-wp-cache update`: Enable and use the cache.
- `-wp-model real+Cast`: Enable the real model to represent the
arithmetic on floating-point numbers. The `Cast` option enables
the usage of cast in the code.
- `-wp-prover alt-ergo,cvc4-strings-ce,z3,z3-ce,z3-nobv,tip`:
Add the different provers needed to verify the goals.
- `-cpp-extra-args=-I../include`: Add the include directory of
Paparazzi.
- `-cpp-extra-args=-DFRAMA_C_ANALYSIS`: Defined a C constant
in order to remove certain portions of code that are not
supported by Frama-C.
More information about Paparazzi
--------------------------------
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment