Skip to content

GitLab

Commit 98300a48 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Merging master

parents cf07e71a 503e4737
Hide whitespace changes
Inline Side-by-side
Showing with 54 additions and 168 deletions
README.md
View file @ 98300a48
# 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:
-------------
```
......@@ -45,7 +48,7 @@ SMOKE=1 ./frama-c-analysis.sh
```
Quick descritpion of modified files:
----------------------------------------
------------------------------------
- `sw/airborne/frama-c-analysis.sh`: Script to automatically
launch the verification using Frama-C.
......@@ -63,19 +66,33 @@ 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
-----------------
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
--------------------------------
......
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
View file @ 98300a48
......@@ -89,5 +89,5 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.364,
"steps": 992 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 1.5505,
"steps": 989 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
View file @ 98300a48
......@@ -36,5 +36,5 @@
{ "Unfold 'L_trace_2_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.5319,
"steps": 1252 } ] } } ] } } ] } } ] } } ]
"time": 2.7065,
"steps": 1249 } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
View file @ 98300a48
......@@ -58,8 +58,8 @@
{ "Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.5305,
"steps": 1013 },
"time": 2.4316,
"steps": 1008 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
......
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
View file @ 98300a48
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_1 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children": { "Unfold 'L_l_RMat_of_FloatRMat'": [ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select": { "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(P_rotation_matrix\n {\n F12_RealRMat_s_a00 = Mf32_1[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_1[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_1[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_1[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_1[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_1[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_1[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_1[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_1[(shift_float32 a_0 8)]\n })",
"pattern": "P_rotation_matrix{RealRMat_s}[][]" },
"children": { "Unfold 'P_rotation_matrix'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(L_transpose\n {\n F12_RealRMat_s_a00 = Mf32_1[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_1[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_1[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_1[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_1[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_1[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_1[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_1[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_1[(shift_float32 a_0 8)]\n })",
"pattern": "L_transpose{RealRMat_s}[][][][][]" },
"children":
{ "Unfold 'L_transpose'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_1[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_1[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_1[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_1[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_1[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_1[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_1[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_1[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_1[(shift_float32 a_0 8)] in\n(L_mult_RealRMat\n {\n F12_RealRMat_s_a00 = r_0 ;\n F12_RealRMat_s_a01 = r_1 ;\n F12_RealRMat_s_a02 = r_2 ;\n F12_RealRMat_s_a10 = r_3 ;\n F12_RealRMat_s_a11 = r_4 ;\n F12_RealRMat_s_a12 = r_5 ;\n F12_RealRMat_s_a20 = r_6 ;\n F12_RealRMat_s_a21 = r_7 ;\n F12_RealRMat_s_a22 = r_8\n }\n {\n F12_RealRMat_s_a00 = r_0 ;\n F12_RealRMat_s_a01 = r_3 ;\n F12_RealRMat_s_a02 = r_6 ;\n F12_RealRMat_s_a10 = r_1 ;\n F12_RealRMat_s_a11 = r_4 ;\n F12_RealRMat_s_a12 = r_7 ;\n F12_RealRMat_s_a20 = r_2 ;\n F12_RealRMat_s_a21 = r_5 ;\n F12_RealRMat_s_a22 = r_8\n })",
"pattern": "L_mult_RealRMat{RealRMat_s}{RealRMat_s}" },
"children":
{ "Unfold 'L_mult_RealRMat'":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 8,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n0<\n(Mf32_1[(shift_float32 a_0 0)]+Mf32_1[(shift_float32 a_0 4)]+\n Mf32_1[(shift_float32 a_0 8)])",
"pattern": "<0+[][][]$Mf32shift_float32$Mf32" },
"children":
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.5,
"steps": 431175 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 10,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nMf32_1[(shift_float32 a_0 4)]<Mf32_1[(shift_float32 a_0 0)]",
"pattern": "<[][]$Mf32shift_float32$Mf32shift_float32" },
"children":
{ "Then":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 12,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nMf32_1[(shift_float32 a_0 8)]<Mf32_1[(shift_float32 a_0 0)]",
"pattern": "<[][]$Mf32shift_float32$Mf32shift_float32" },
"children":
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.39,
"steps": 395604 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 16,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nMf32_1[(shift_float32 a_0 8)]<Mf32_1[(shift_float32 a_0 4)]",
"pattern": "<[][]$Mf32shift_float32$Mf32shift_float32" },
"children":
{ "Then":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.08,
"steps": 223243 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.36,
"steps": 394729 } ] } } ] } } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 13,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nMf32_1[(shift_float32 a_0 8)]<Mf32_1[(shift_float32 a_0 4)]",
"pattern": "<[][]$Mf32shift_float32$Mf32shift_float32" },
"children":
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.39,
"steps": 395218 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.4,
"steps": 392197 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-step", "at": 8, "kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n0<\n(Mf32_1[(shift_float32 a_0 0)]+Mf32_1[(shift_float32 a_0 4)]+\n Mf32_1[(shift_float32 a_0 8)])",
"pattern": "<0+[][][]$Mf32shift_float32$Mf32" },
"children": { "Then": [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid", "time": 0.31,
"steps": 404607 } ],
"Else": [ { "prover": "Alt-Ergo:2.3.3", "verdict": "valid",
"time": 3.7782, "steps": 1331 } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_2.json
View file @ 98300a48
[ { "header": "Filter", "tactic": "Wp.filter", "params": { "anti": false },
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(P_rotation_matrix (L_l_RMat_of_FloatRMat Mf32_1 rm_0))",
"pattern": "P_rotation_matrixL_l_RMat_of_FloatRMat" },
"children": { "Filter": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 6.2335,
"steps": 1628 } ] } } ]
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-step", "at": 8, "kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n0<\n(Mf32_1[(shift_float32 a_0 0)]+Mf32_1[(shift_float32 a_0 4)]+\n Mf32_1[(shift_float32 a_0 8)])",
"pattern": "<0+[][][]$Mf32shift_float32$Mf32" },
"children": { "Then": [ { "prover": "Alt-Ergo:2.3.3", "verdict": "valid",
"time": 0.7925, "steps": 722 } ],
"Else": [ { "prover": "Alt-Ergo:2.3.3", "verdict": "valid",
"time": 4.5395, "steps": 1331 } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_trace_pos_ensures.json
View file @ 98300a48
......@@ -79,5 +79,5 @@
{ "Unfold 'EqS13_RealQuat_s'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 7.3667,
"steps": 4632 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 9.5815,
"steps": 4599 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/math/pprz_algebra_float.c
View file @ 98300a48
......@@ -608,25 +608,6 @@ void float_quat_of_orientation_vect(struct FloatQuat *q, const struct FloatVect3
}
}
/*
lemma test:
\forall real r_5, r_6, r_12, r_13, r_14, r_15, r_16, r_17;
SQR(r_5) / 4
+ SQR((r_14 - r_12) / (2 * r_5)) + SQR((r_13 - r_16) / (2 * r_5)) + SQR((r_17 - r_15) / (2 * r_5)) == 1.0;
*/
/*
lemma test_2:
\forall struct FloatRMat *rm;
\let r_4 = 1.0 + rm->m[0] + rm->m[4] + rm->m[8];
\let r_5 = \sqrt(r_4);
\let r_6 = 2.0 * r_5;
\valid_read(rm) ==>
((1.0/4) * r_5 * r_5
+ SQR((rm->m[5] - rm->m[7]) / (r_6))
+ SQR((rm->m[6] - rm->m[2]) / (r_6))
+ SQR((rm->m[1] - rm->m[3]) / (r_6))) == 1.0;
*/
void float_quat_of_rmat(struct FloatQuat *q, struct FloatRMat *rm)
{
......
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