Commit b9731716 authored by GARION Christophe's avatar GARION Christophe
Browse files

fmics21: update README, correct typos and add links to verified functions

parent a5cb0535
Frama-C Verification of Paparazzi
=================================
This GitLab project is a fork of Paparazzi UAV autopilot
(https://github.com/paparazzi/paparazzi) that verify
`pprz_algebra` library using Frama-C.
This project adds the ACSL annotations in the code and provide a
script to automatically launch the verification. Frama-C
analyses the code and checks the absence of RTE (_RunTime
Errors_) and some functional properties.
This GitLab repository is a fork of Paparazzi UAV autopilot repository
(https://github.com/paparazzi/paparazzi). The aim of this project is
to verify the `pprz_algebra` library using Frama-C.
This project adds ACSL annotations and provides a script to
automatically launch Frama-C. Frama-C analyses the code, checks for
the absence of RTE (_RunTime Errors_) and verify some functional
properties.
Required software
-----------------
......@@ -26,81 +27,102 @@ 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:
How to launch the verification process
-------------
First, go to the `sw/airborne` directory:
```
cd sw/airborne
```
Update the variable `FRAMAC_PREFIX` in `frama-c-analysis.sh`
with the path of the directory containing Frama-C binary. Then,
launch the script that start the analysis:
launch the script that starts the analysis:
```
./frama-c-analysis.sh
```
The WP smoke tests can be enable with the environment variable
`SMOKE` as follow:
The WP smoke tests can be enabled with the environment variable
`SMOKE` as follows:
```
SMOKE=1 ./frama-c-analysis.sh
```
Quick descritpion of modified files:
Quick description of modified files
------------------------------------
- `sw/airborne/frama-c-analysis.sh`: Script to automatically
launch the verification using Frama-C.
- `sw/airborne/output-frama-c-analysis.sh`: A python script
used by `frama-c-analysis.sh` to read and analyse the results
from Frama-C.
- `sw/airborne/math/pprz_algebra_(int|float|double).(h|c)`:
Mathematical library of Paparazzi that has been verified. These
files have been annotated with ACSL.
- `sw/airborne/math/pprz_algebra_(int|float|double)_frama_c.h`:
Files containing definition of predicates, lemma and logical
functions used to verify the absence of RTE in the library.
- `sw/airborne/frama-c-analysis.sh`: a shell script that automatically
launches the verification using Frama-C.
- `sw/airborne/output-frama-c-analysis.sh`: a Python script used by
`frama-c-analysis.sh` to read and analyse the results from Frama-C.
- `sw/airborne/math/pprz_algebra_(int|float|double).(h|c)`: the
mathematical library of Paparazzi that has been verified. These files
have been annotated with ACSL.
- `sw/airborne/math/pprz_algebra_(int|float|double)_frama_c.h`: files
containing definition of predicates, lemmas and logical functions used
to verify the absence of RTE in the library.
- `sw/airborne/math/pprz_algebra_float_convert_rmat_frama_c.h`:
Definition of predicates, lemma and logical functions for the
definition of predicates, lemmas and logical functions for the
verification of functional properties.
- `sw/airborne/.frama-c/wp/interactive`: All the Coq scripts
containing the proof of certain lemma.
- `sw/airborne/.frama-c/wp/script`: All WP scripts containing
the tactics used to prove some goals.
- `sw/airborne/.frama-c/wp/interactive`: Coq scripts containing the
proof lemmas.
- `sw/airborne/.frama-c/wp/script`: WP scripts containing the tactics
used to prove some goals.
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 Frama-C verification is
launched for every function `FUNCTION` with the following
parameters:
- `-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
Verification process
---------------------
The verification process 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 of Frama-C. The
EVA plugin requires a program entry point (a `main` or a function) to
start its analysis. The script `frama-c-analysis.sh` finds
automatically all the names of the functions in the library using
ctags. Then, verification is launched for every function `FUNCTION`
with the following parameters:
- `-rte`: adds RTE annotations in the code.
- `-no-warn-left-shift-negative`: allows left shift for negative values.
- `-eva -lib-entry -main $FUNCTION`: launches 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.
the _preconditions_ specified in the contract of the function.
- `-wp-fct $FUNCTION`: launches the WP verification with the following
options:
- `-wp-cache update`: enables and uses cache.
- `-wp-model real+Cast`: enables 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
adds the different provers needed to verify the goals.
- `-cpp-extra-args=-I../include`: adds 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.
- `-cpp-extra-args=-DFRAMA_C_ANALYSIS`: defines a C constant in order
to remove certain portions of code that are not supported by
Frama-C.
Quick link to functions described in FMICS 2021 paper
-----------------------------------------------------
- the
[`float_rmat\_of_quat`](https://gitlab.isae-supaero.fr/b.pollien/paparazzi-frama-c/-/blob/fmics-2021/sw/airborne/math/pprz_algebra_float.h#L633)
function
- the
[`float_quat_of_rmat`](https://gitlab.isae-supaero.fr/b.pollien/paparazzi-frama-c/-/blob/fmics-2021/sw/airborne/math/pprz_algebra_float.h#L946)
function
- the
[`float_rmat_of_eulers_321`](https://gitlab.isae-supaero.fr/b.pollien/paparazzi-frama-c/-/blob/fmics-2021/sw/airborne/math/pprz_algebra_float.h#L612)
function
- the
[`float_rmat_of_eulers_312`](https://gitlab.isae-supaero.fr/b.pollien/paparazzi-frama-c/-/blob/fmics-2021/sw/airborne/math/pprz_algebra_float.h#L620)
function
More information about Paparazzi
--------------------------------
To have information about Paparazzi, go directly on the
[website](https://wiki.paparazziuav.org/wiki/Main_Page) or on
the [GitLab project](https://github.com/paparazzi/paparazzi).
\ No newline at end of file
[website](https://wiki.paparazziuav.org/wiki/Main_Page) or on the
[GitLab project](https://github.com/paparazzi/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