Commit 31c488d6 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Merge branch 'master' into functional-verification

parents e67a1d30 704419ec
......@@ -64,6 +64,10 @@ 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
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.
The verification:
-----------------
......
......@@ -89,5 +89,5 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.4631,
"time": 1.3969,
"steps": 992 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -36,5 +36,5 @@
{ "Unfold 'L_trace_2_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.9531,
"time": 3.0198,
"steps": 1252 } ] } } ] } } ] } } ] } } ]
......@@ -58,7 +58,7 @@
{ "Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.4767,
"time": 2.5554,
"steps": 1013 },
{ "header": "Definition",
"tactic": "Wp.unfold",
......
......@@ -49,8 +49,8 @@
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.31,
"steps": 431175 } ],
"time": 0.35,
"steps": 431323 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
......@@ -76,8 +76,8 @@
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.33,
"steps": 395604 } ],
"time": 0.48,
"steps": 395625 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
......@@ -92,13 +92,13 @@
{ "Then":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.05,
"steps": 223243 } ],
"time": 0.08,
"steps": 226918 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.4,
"steps": 394729 } ] } } ] } } ],
"steps": 395020 } ] } } ] } } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
......@@ -113,10 +113,10 @@
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.32,
"steps": 395218 } ],
"time": 0.4,
"steps": 395380 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.34,
"steps": 392197 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 0.37,
"steps": 392223 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -3,5 +3,5 @@
"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": 5.4931,
"verdict": "valid", "time": 5.4734,
"steps": 1628 } ] } } ]
......@@ -79,5 +79,5 @@
{ "Unfold 'EqS13_RealQuat_s'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 8.3262,
"time": 7.162,
"steps": 4632 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -59,30 +59,30 @@
{ "Goal 1/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.4375,
"time": 1.4602,
"steps": 102 } ],
"Goal 2/6":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.66,
"steps": 2414090 } ],
"time": 0.45,
"steps": 2417925 } ],
"Goal 3/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.4657,
"time": 2.0874,
"steps": 102 } ],
"Goal 4/6":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.56,
"steps": 2414075 } ],
"time": 0.55,
"steps": 2417912 } ],
"Goal 5/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.2324,
"time": 1.632,
"steps": 102 } ],
"Goal 6/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.0371,
"time": 1.5937,
"steps": 102 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -11,5 +11,5 @@
"children": { "Unfold 'P_special_orthogonal'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.1125,
"time": 1.8127,
"steps": 102 } ] } } ] } } ]
......@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 0.89 } ],
"verdict": "valid", "time": 1.06 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.23 } ],
"verdict": "valid", "time": 4. } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.18 } ],
"verdict": "valid", "time": 3.84 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
......@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 3.64 } ],
"verdict": "valid", "time": 3.34 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.3 } ],
"verdict": "valid", "time": 6.26 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.38 } ],
"verdict": "valid", "time": 5.88 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(P_unary_quaternion_1_ Mf32_1 q_0)",
"pattern": "P_unary_quaternion_1_$Mf32$q" },
"children": { "Unfold 'P_unary_quaternion_1_'": [ { "header": "Separated",
"tactic": "Wp.separated",
"params": {},
"select": { "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 2.3 } ],
"OnLeft":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 5.51 } ],
"OnRight":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 4.29 } ],
"OverLap":
[ { "prover": "qed",
"verdict": "valid" } ] } } ] } } ]
......@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.8 } ],
"verdict": "valid", "time": 5.62 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 8.96 } ],
"verdict": "valid", "time": 11.86 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 8.91 } ],
"verdict": "valid", "time": 9.64 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
[ { "prover": "script", "verdict": "valid" },
{ "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-goal", "occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_1[(shiftfield_F7_FloatQuat_qi q_0)] in\nlet r_1 = (2*r_0*r_0) in\nlet r_2 = Mf32_1[(shiftfield_F7_FloatQuat_qx q_0)] in\nlet r_3 = Mf32_1[(shiftfield_F7_FloatQuat_qz q_0)] in\nlet r_4 = (2*r_0*r_3) in\nlet r_5 = Mf32_1[(shiftfield_F7_FloatQuat_qy q_0)] in\nlet r_6 = (2*r_2*r_5) in\nlet r_7 = (2*r_0*r_5) in\nlet r_8 = (2*r_2*r_3) in\nlet r_9 = (2*r_0*r_2) in\nlet r_10 = (2*r_5*r_3) in\n(L_transpose\n (L_l_RMat_of_FloatRMat\n Mf32_1[(shift_float32 a_0 0)->r_1+(2*r_2*r_2)-1][(shift_float32 a_0 1)\n ->r_4+r_6][(shift_float32 a_0 2)->r_8-r_7][(shift_float32 a_0 3)\n ->r_6-r_4][(shift_float32 a_0 4)->r_1+(2*r_5*r_5)-1]\n [(shift_float32 a_0 5)->r_9+r_10][(shift_float32 a_0 6)->r_7+r_8]\n [(shift_float32 a_0 7)->r_10-r_9][(shift_float32 a_0 8)\n ->r_1+(2*r_3*r_3)-1] rm_0))",
"pattern": "L_transposeL_l_RMat_of_FloatRMat" },
......@@ -10,6 +11,62 @@
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_1[(shiftfield_F7_FloatQuat_qi q_0)] in\nlet r_1 = (2*r_0*r_0) in\nlet r_2 = Mf32_1[(shiftfield_F7_FloatQuat_qx q_0)] in\nlet r_3 = Mf32_1[(shiftfield_F7_FloatQuat_qz q_0)] in\nlet r_4 = (2*r_0*r_3) in\nlet r_5 = Mf32_1[(shiftfield_F7_FloatQuat_qy q_0)] in\nlet r_6 = (2*r_2*r_5) in\nlet r_7 = (2*r_0*r_5) in\nlet r_8 = (2*r_2*r_3) in\nlet r_9 = (2*r_0*r_2) in\nlet r_10 = (2*r_5*r_3) in\n(L_l_RMat_of_FloatQuat_1_\n Mf32_1[(shift_float32 a_0 0)->r_1+(2*r_2*r_2)-1][(shift_float32 a_0 1)\n ->r_4+r_6][(shift_float32 a_0 2)->r_8-r_7][(shift_float32 a_0 3)\n ->r_6-r_4][(shift_float32 a_0 4)->r_1+(2*r_5*r_5)-1]\n [(shift_float32 a_0 5)->r_9+r_10][(shift_float32 a_0 6)->r_7+r_8]\n [(shift_float32 a_0 7)->r_10-r_9][(shift_float32 a_0 8)\n ->r_1+(2*r_3*r_3)-1] q_0)",
"pattern": "L_l_RMat_of_FloatQuat_1_[=]$q[=]" },
"children": { "Unfold 'L_l_RMat_of_FloatQuat_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 3.24 } ] } } ] } } ]
[ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout",
"time": 10. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "timeout",
"time": 10. },
{ "prover": "Z3:4.8.6",
"verdict": "timeout",
"time": 10. },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout",
"time": 10. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 10. },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "clause-goal",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_1[(shiftfield_F7_FloatQuat_qi q_0)] in\nlet r_1 = (2*r_0*r_0) in\nlet r_2 = Mf32_1[(shiftfield_F7_FloatQuat_qx q_0)] in\nlet r_3 = Mf32_1[(shiftfield_F7_FloatQuat_qz q_0)] in\nlet r_4 = (2*r_0*r_3) in\nlet r_5 = Mf32_1[(shiftfield_F7_FloatQuat_qy q_0)] in\nlet r_6 = (2*r_2*r_5) in\nlet r_7 = (2*r_0*r_5) in\nlet r_8 = (2*r_2*r_3) in\nlet r_9 = (2*r_0*r_2) in\nlet r_10 = (2*r_5*r_3) in\nlet a_1 =\n (L_l_RMat_of_FloatRMat\n Mf32_1[(shift_float32 a_0 0)->r_1+(2*r_2*r_2)-1][(shift_float32 a_0 1)\n ->r_4+r_6][(shift_float32 a_0 2)->r_8-r_7][(shift_float32 a_0 3)\n ->r_6-r_4][(shift_float32 a_0 4)->r_1+(2*r_5*r_5)-1]\n [(shift_float32 a_0 5)->r_9+r_10][(shift_float32 a_0 6)->r_7+r_8]\n [(shift_float32 a_0 7)->r_10-r_9][(shift_float32 a_0 8)\n ->r_1+(2*r_3*r_3)-1] rm_0) in\nlet r_11 = (r_5*r_5) in\nlet r_12 = (-r_11) in\nlet r_13 = (r_3*r_3) in\nlet r_14 = (-r_13) in\nlet r_15 = (r_0*r_0) in\nlet r_16 = (r_2*r_2) in\nlet r_17 = (r_0*r_3) in\nlet r_18 = (r_2*r_5) in\nlet r_19 = (r_0*r_5) in\nlet r_20 = (r_2*r_3) in\nlet r_21 = (-r_16) in\nlet r_22 = (r_0*r_2) in\nlet r_23 = (r_5*r_3) in\n(EqS12_RealRMat_s\n {\n a_1 with\n F12_RealRMat_s_a01 = a_1.F12_RealRMat_s_a10 ;\n F12_RealRMat_s_a02 = a_1.F12_RealRMat_s_a20 ;\n F12_RealRMat_s_a10 = a_1.F12_RealRMat_s_a01 ;\n F12_RealRMat_s_a12 = a_1.F12_RealRMat_s_a21 ;\n F12_RealRMat_s_a20 = a_1.F12_RealRMat_s_a02 ;\n F12_RealRMat_s_a21 = a_1.F12_RealRMat_s_a12\n }\n {\n F12_RealRMat_s_a00 = r_15+r_16-r_11-r_13 ;\n F12_RealRMat_s_a01 = 2*(r_18-r_17) ;\n F12_RealRMat_s_a02 = 2*(r_19+r_20) ;\n F12_RealRMat_s_a10 = 2*(r_17+r_18) ;\n F12_RealRMat_s_a11 = r_15+r_11-r_16-r_13 ;\n F12_RealRMat_s_a12 = 2*(r_23-r_22) ;\n F12_RealRMat_s_a20 = 2*(r_20-r_19) ;\n F12_RealRMat_s_a21 = 2*(r_22+r_23) ;\n F12_RealRMat_s_a22 = r_15+r_13-r_16-r_11\n })",
"pattern": "EqS12_RealRMat_s{RealRMat_s}{RealRMat_s}" },
"children":
{ "Unfold 'EqS12_RealRMat_s'":
[ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout",
"time": 10. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "timeout",
"time": 10. },
{ "prover": "Z3:4.8.6",
"verdict": "timeout",
"time": 10. },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout",
"time": 10. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 10. },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-goal",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_1[(shiftfield_F7_FloatQuat_qi q_0)] in\nlet r_1 = (2*r_0*r_0) in\nlet r_2 = Mf32_1[(shiftfield_F7_FloatQuat_qx q_0)] in\nlet r_3 = Mf32_1[(shiftfield_F7_FloatQuat_qz q_0)] in\nlet r_4 = (2*r_0*r_3) in\nlet r_5 = Mf32_1[(shiftfield_F7_FloatQuat_qy q_0)] in\nlet r_6 = (2*r_2*r_5) in\nlet r_7 = (2*r_0*r_5) in\nlet r_8 = (2*r_2*r_3) in\nlet r_9 = (2*r_0*r_2) in\nlet r_10 = (2*r_5*r_3) in\n(L_l_RMat_of_FloatRMat\n Mf32_1[(shift_float32 a_0 0)->r_1+(2*r_2*r_2)-1][(shift_float32 a_0 1)\n ->r_4+r_6][(shift_float32 a_0 2)->r_8-r_7][(shift_float32 a_0 3)\n ->r_6-r_4][(shift_float32 a_0 4)->r_1+(2*r_5*r_5)-1]\n [(shift_float32 a_0 5)->r_9+r_10][(shift_float32 a_0 6)->r_7+r_8]\n [(shift_float32 a_0 7)->r_10-r_9][(shift_float32 a_0 8)\n ->r_1+(2*r_3*r_3)-1] rm_0)",
"pattern": "L_l_RMat_of_FloatRMat[=]$rm[=]shift_float32" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.03,
"steps": 125856 },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" } ] } } ] } } ] } } ] } } ]
......@@ -72,7 +72,7 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.48 } ] } } ],
"time": 1.96 } ] } } ],
"Goal 2/6":
[ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -88,7 +88,7 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.7839,
"time": 1.9381,
"steps": 28 } ] } } ],
"Goal 3/6":
[ { "header": "Definition",
......@@ -105,7 +105,7 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.07 } ] } } ],
"time": 1.22 } ] } } ],
"Goal 4/6":
[ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -137,7 +137,7 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 2.18 } ] } } ],
"time": 2.17 } ] } } ],
"Goal 6/6":
[ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -153,7 +153,7 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.5372,
"time": 2.664,
"steps": 28 },
{ "header": "Definition",
"tactic": "Wp.unfold",
......
......@@ -33,5 +33,5 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 3.0835,
"time": 3.2164,
"steps": 28 } ] } } ] } } ] } } ] } } ]
......@@ -63,5 +63,5 @@
{ "Unfold 'EqS12_RealRMat_s'":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.02,
"steps": 45566 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 0.04,
"steps": 46240 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -193,9 +193,7 @@ void float_rmat_of_axis_angle(struct FloatRMat *rm, struct FloatVect3 *uv, float
void float_rmat_of_eulers_321(struct FloatRMat *rm, struct FloatEulers *e)
{
const float sphi = sinf(e->phi);
//@ assert sphi == \sin(e->phi);
const float cphi = cosf(e->phi);
//@assert cphi == \cos(e->phi);
const float stheta = sinf(e->theta);
const float ctheta = cosf(e->theta);
const float spsi = sinf(e->psi);
......
......@@ -301,6 +301,13 @@ logic RealRMat l_RMat_of_FloatQuat(RealQuat q) =
==> rotation_matrix(l_RMat_of_FloatQuat(q));
*/
/*@
lemma quat_of_rmat_special_ortho:
\forall struct FloatQuat *q;
unary_quaternion(q)
==> special_orthogonal(l_RMat_of_FloatQuat(q));
*/
/*******************************
* CONVERT RMAT TO QUAT
* *****************************/
......
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