Skip to content

GitLab

Commit 756f5bc0 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Update script

parent 085c1207
Show whitespace changes
Inline Side-by-side
Showing with 64 additions and 157 deletions
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
View file @ 756f5bc0
......@@ -32,33 +32,6 @@
"pattern": "L_l_FloatQuat_of_RMat_0_max_1_{RealRMat_s}" },
"children":
{ "Unfold 'L_l_FloatQuat_of_RMat_0_max_1_'":
[ { "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.6951,
"steps": 1663 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "clause-goal",
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 =\n (\\sqrt\n (1+Mf32_0[(shift_float32 a_0 0)]-Mf32_0[(shift_float32 a_0 4)]-\n Mf32_0[(shift_float32 a_0 8)])) in\nlet r_1 = (2*r_0) in\n(EqS10_RealQuat_s\n {\n F10_RealQuat_s_qi =\n (Mf32_0[(shift_float32 a_0 5)]-Mf32_0[(shift_float32 a_0 7)]) div r_1 ;\n F10_RealQuat_s_qx = 1/2*r_0 ;\n F10_RealQuat_s_qy =\n (Mf32_0[(shift_float32 a_0 1)]+Mf32_0[(shift_float32 a_0 3)]) div r_1 ;\n F10_RealQuat_s_qz =\n (Mf32_0[(shift_float32 a_0 2)]+Mf32_0[(shift_float32 a_0 6)]) div r_1\n } (L_l_Quat_of_FloatQuat Mf32_0 q_0))",
"pattern": "EqS10_RealQuat_s{RealQuat_s}L_l_Quat_of_FloatQuat" },
"children":
{ "Unfold 'EqS10_RealQuat_s'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
......@@ -69,43 +42,7 @@
"pattern": "L_l_Quat_of_FloatQuat$Mf32$q" },
"children":
{ "Unfold 'L_l_Quat_of_FloatQuat'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_27 rm_0)",
"pattern": "L_trace_2_$Mf32$rm" },
"children":
{ "Unfold 'L_trace_2_'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_27 rm_0))",
"pattern": "L_trace_1_L_l_RMat_of_FloatRMat$Mf32" },
"children":
{ "Unfold 'L_trace_1_'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_27 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 4.9965,
"steps": 1942 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 9.5682,
"steps": 1715 } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
View file @ 756f5bc0
......@@ -24,8 +24,8 @@
{ "Unfold 'L_l_FloatQuat_of_RMat_1_max_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 7.8582,
"steps": 1632 },
"time": 8.7286,
"steps": 1690 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
......
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
View file @ 756f5bc0
......@@ -58,8 +58,8 @@
{ "Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.0645,
"steps": 1001 },
"time": 2.96,
"steps": 1275 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
......
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
View file @ 756f5bc0
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_5 rm_0)",
"target": "(L_l_RMat_of_FloatRMat Mf32_6 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children": { "Unfold 'L_l_RMat_of_FloatRMat'": [ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -9,7 +9,7 @@
"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_5[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_5[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_5[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_5[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_5[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_5[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_5[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_5[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_5[(shift_float32 a_0 8)]\n })",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(P_rotation_matrix\n {\n F12_RealRMat_s_a00 = Mf32_6[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_6[(shift_float32 a_0 8)]\n })",
"pattern": "P_rotation_matrix{RealRMat_s}[][]" },
"children": { "Unfold 'P_rotation_matrix'":
[ { "header": "Definition",
......@@ -20,7 +20,7 @@
"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_5[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_5[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_5[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_5[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_5[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_5[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_5[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_5[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_5[(shift_float32 a_0 8)]\n })",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(L_transpose\n {\n F12_RealRMat_s_a00 = Mf32_6[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_6[(shift_float32 a_0 8)]\n })",
"pattern": "L_transpose{RealRMat_s}[][][][][]" },
"children":
{ "Unfold 'L_transpose'":
......@@ -32,16 +32,13 @@
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_5[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_5[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_5[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_5[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_5[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_5[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_5[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_5[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_5[(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 })",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_6[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_6[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_6[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_6[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_6[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_6[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_6[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_6[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_6[(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'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 0.25 },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 10. },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
......
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_12.json 0 → 100644
View file @ 756f5bc0
[ { "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. } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_13.json 0 → 100644
View file @ 756f5bc0
[ { "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. } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_14.json 0 → 100644
View file @ 756f5bc0
[ { "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. } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_15.json 0 → 100644
View file @ 756f5bc0
[ { "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. } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_2.json
View file @ 756f5bc0
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_5 rm_0)",
"target": "(L_l_RMat_of_FloatRMat Mf32_6 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children": { "Unfold 'L_l_RMat_of_FloatRMat'": [ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -9,7 +9,7 @@
"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_5[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_5[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_5[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_5[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_5[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_5[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_5[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_5[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_5[(shift_float32 a_0 8)]\n })",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(P_rotation_matrix\n {\n F12_RealRMat_s_a00 = Mf32_6[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_6[(shift_float32 a_0 8)]\n })",
"pattern": "P_rotation_matrix{RealRMat_s}[][]" },
"children": { "Unfold 'P_rotation_matrix'":
[ { "header": "Definition",
......@@ -20,7 +20,7 @@
"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_5[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_5[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_5[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_5[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_5[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_5[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_5[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_5[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_5[(shift_float32 a_0 8)]\n })",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(L_transpose\n {\n F12_RealRMat_s_a00 = Mf32_6[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_6[(shift_float32 a_0 8)]\n })",
"pattern": "L_transpose{RealRMat_s}[][][][][]" },
"children":
{ "Unfold 'L_transpose'":
......@@ -44,16 +44,13 @@
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_5[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_5[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_5[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_5[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_5[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_5[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_5[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_5[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_5[(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 })",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_6[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_6[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_6[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_6[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_6[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_6[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_6[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_6[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_6[(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'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 9.1 },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 10. },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
......
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_ensures.json
View file @ 756f5bc0
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 10. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. },
{ "prover": "script", "verdict": "timeout", "time": 10. },
{ "header": "Definition", "tactic": "Wp.unfold", "params": {},
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-goal",
"target": "(P_unary_quaterion Mf32_0 q_0)",
"pattern": "P_unary_quaterion$Mf32$q" },
"children": { "Unfold 'P_unary_quaterion'": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout",
"time": 10. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 10. },
{ "header": "Definition",
"children": { "Unfold 'P_unary_quaterion'": [ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select": { "select": "inside-step",
"at": 2,
"at": 3,
"kind": "have",
"occur": 0,
"target": "(P_rotation_matrix (L_l_RMat_of_FloatRMat Mf32_27 rm_0))",
"target": "(P_rotation_matrix (L_l_RMat_of_FloatRMat Mf32_1 rm_0))",
"pattern": "P_rotation_matrixL_l_RMat_of_FloatRMat" },
"children": { "Unfold 'P_rotation_matrix'":
[ { "header": "Definition",
......@@ -27,10 +17,10 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_transpose (L_l_RMat_of_FloatRMat Mf32_27 rm_0))",
"target": "(L_transpose (L_l_RMat_of_FloatRMat Mf32_1 rm_0))",
"pattern": "L_transposeL_l_RMat_of_FloatRMat" },
"children":
{ "Unfold 'L_transpose'":
......@@ -39,14 +29,17 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"at": 3,
"kind": "have",
"occur": 0,
"target": "let a_0 = (L_l_RMat_of_FloatRMat Mf32_27 rm_0) in\n(L_mult_RealRMat a_0\n {\n a_0 with\n F9_RealRMat_s_a01 = a_0.F9_RealRMat_s_a10 ;\n F9_RealRMat_s_a02 = a_0.F9_RealRMat_s_a20 ;\n F9_RealRMat_s_a10 = a_0.F9_RealRMat_s_a01 ;\n F9_RealRMat_s_a12 = a_0.F9_RealRMat_s_a21 ;\n F9_RealRMat_s_a20 = a_0.F9_RealRMat_s_a02 ;\n F9_RealRMat_s_a21 = a_0.F9_RealRMat_s_a12\n })",
"target": "let a_0 = (L_l_RMat_of_FloatRMat Mf32_1 rm_0) in\n(L_mult_RealRMat a_0\n {\n a_0 with\n F12_RealRMat_s_a01 = a_0.F12_RealRMat_s_a10 ;\n F12_RealRMat_s_a02 = a_0.F12_RealRMat_s_a20 ;\n F12_RealRMat_s_a10 = a_0.F12_RealRMat_s_a01 ;\n F12_RealRMat_s_a12 = a_0.F12_RealRMat_s_a21 ;\n F12_RealRMat_s_a20 = a_0.F12_RealRMat_s_a02 ;\n F12_RealRMat_s_a21 = a_0.F12_RealRMat_s_a12\n })",
"pattern": "L_mult_RealRMatL_l_RMat_of_FloatRMat" },
"children":
{ "Unfold 'L_mult_RealRMat'":
[ { "header": "Definition",
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 0.55 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
......
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_trace_pos_ensures.json
View file @ 756f5bc0
......@@ -32,52 +32,6 @@
"pattern": "L_l_Quat_of_FloatQuat$Mf32$q" },
"children":
{ "Unfold 'L_l_Quat_of_FloatQuat'":
[ { "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 = (L_l_RMat_of_FloatRMat Mf32_0 rm_0) in\n(L_trace_1_\n {\n a_0 with\n F9_RealRMat_s_a01 = a_0.F9_RealRMat_s_a10 ;\n F9_RealRMat_s_a02 = a_0.F9_RealRMat_s_a20 ;\n F9_RealRMat_s_a10 = a_0.F9_RealRMat_s_a01 ;\n F9_RealRMat_s_a12 = a_0.F9_RealRMat_s_a21 ;\n F9_RealRMat_s_a20 = a_0.F9_RealRMat_s_a02 ;\n F9_RealRMat_s_a21 = a_0.F9_RealRMat_s_a12\n })",
"pattern": "L_trace_1_{RealRMat_s}.F9_RealRMat_s_a00" },
"children":
{ "Unfold 'L_trace_1_'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "clause-goal",
"target": "let a_0 = (L_l_RMat_of_FloatRMat Mf32_0 rm_0) in\nlet r_0 =\n (1/2\n div (\\sqrt\n (1+a_0.F9_RealRMat_s_a00+a_0.F9_RealRMat_s_a11+\n a_0.F9_RealRMat_s_a22))) in\n(EqS10_RealQuat_s\n {\n F10_RealQuat_s_qi = 1/4 div r_0 ;\n F10_RealQuat_s_qx = (a_0.F9_RealRMat_s_a12-a_0.F9_RealRMat_s_a21)*r_0 ;\n F10_RealQuat_s_qy = (a_0.F9_RealRMat_s_a20-a_0.F9_RealRMat_s_a02)*r_0 ;\n F10_RealQuat_s_qz = (a_0.F9_RealRMat_s_a01-a_0.F9_RealRMat_s_a10)*r_0\n }\n {\n F10_RealQuat_s_qi = Mf32_0[(shiftfield_F4_FloatQuat_qi q_0)] ;\n F10_RealQuat_s_qx = Mf32_0[(shiftfield_F4_FloatQuat_qx q_0)] ;\n F10_RealQuat_s_qy = Mf32_0[(shiftfield_F4_FloatQuat_qy q_0)] ;\n F10_RealQuat_s_qz = Mf32_0[(shiftfield_F4_FloatQuat_qz q_0)]\n })",
"pattern": "EqS10_RealQuat_s{RealQuat_s}{RealQuat_s}" },
"children":
{ "Unfold 'EqS10_RealQuat_s'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-goal",
"occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_0 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
......@@ -86,7 +40,7 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_27 rm_0)",
"target": "(L_trace_2_ Mf32_1 rm_0)",
"pattern": "L_trace_2_$Mf32$rm" },
"children":
{ "Unfold 'L_trace_2_'":
......@@ -98,7 +52,7 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_27 rm_0))",
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_1 rm_0))",
"pattern": "L_trace_1_L_l_RMat_of_FloatRMat$Mf32" },
"children":
{ "Unfold 'L_trace_1_'":
......@@ -110,11 +64,11 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_27 rm_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'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 4.3424,
"steps": 2277 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 13.0101,
"steps": 844 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/math/pprz_algebra_float.c
View file @ 756f5bc0
......@@ -629,7 +629,7 @@ void float_quat_of_rmat(struct FloatQuat *q, struct FloatRMat *rm)
//@ assert \at(rm->m[7], Pre) == rm->m[7];
//@ assert \at(rm->m[8], Pre) == rm->m[8];
//@ assert SQR(rm->m[0]) + SQR(rm->m[1]) + SQR(rm->m[2]) == 1;
// assert unary_quaterion(q);
//@ assert unary_quaterion(q);
/*printf("tr > 0\n");*/
} else {
if (RMAT_ELMT(*rm, 0, 0) > RMAT_ELMT(*rm, 1, 1) &&
......@@ -641,7 +641,7 @@ void float_quat_of_rmat(struct FloatQuat *q, struct FloatRMat *rm)
q->qx = 0.5 * two_qx;
q->qy = (RMAT_ELMT(*rm, 0, 1) + RMAT_ELMT(*rm, 1, 0)) / four_qx;
q->qz = (RMAT_ELMT(*rm, 2, 0) + RMAT_ELMT(*rm, 0, 2)) / four_qx;
// assert unary_quaterion(q);
//@ assert unary_quaterion(q);
/*printf("m00 largest\n");*/
} else if (RMAT_ELMT(*rm, 1, 1) > RMAT_ELMT(*rm, 2, 2)) {
const float two_qy =
......@@ -651,7 +651,7 @@ void float_quat_of_rmat(struct FloatQuat *q, struct FloatRMat *rm)
q->qx = (RMAT_ELMT(*rm, 0, 1) + RMAT_ELMT(*rm, 1, 0)) / four_qy;
q->qy = 0.5 * two_qy;
q->qz = (RMAT_ELMT(*rm, 1, 2) + RMAT_ELMT(*rm, 2, 1)) / four_qy;
// assert unary_quaterion(q);
//@ assert unary_quaterion(q);
/*printf("m11 largest\n");*/
} else {
const float two_qz =
......@@ -661,7 +661,7 @@ void float_quat_of_rmat(struct FloatQuat *q, struct FloatRMat *rm)
q->qx = (RMAT_ELMT(*rm, 2, 0) + RMAT_ELMT(*rm, 0, 2)) / four_qz;
q->qy = (RMAT_ELMT(*rm, 1, 2) + RMAT_ELMT(*rm, 2, 1)) / four_qz;
q->qz = 0.5 * two_qz;
// assert unary_quaterion(q);
//@ assert unary_quaterion(q);
/*printf("m22 largest\n");*/
}
}
......
sw/airborne/math/pprz_algebra_float.h
View file @ 756f5bc0
......@@ -885,6 +885,7 @@ extern void float_quat_of_orientation_vect(struct FloatQuat *q, const struct Flo
requires rvalid_FloatRMat(rm);
requires rotation_matrix(l_RMat_of_FloatRMat(rm));
requires \separated(rm, q);
ensures unary_quaterion(q);
assigns *q;
behavior trace_pos:
......
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