Skip to content
Snippets Groups Projects
Commit ad08a5d4 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Adding new lemma

parent 32db4336
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 110 additions and 77 deletions
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
+ 1
− 1
View file @ ad08a5d4
......@@ -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 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
+ 1
− 1
View file @ ad08a5d4
......@@ -36,5 +36,5 @@
{ "Unfold 'L_trace_2_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.9531,
"time": 3.0198,
"steps": 1252 } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
+ 1
− 1
View file @ ad08a5d4
......@@ -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",
......
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
+ 11
− 11
View file @ ad08a5d4
......@@ -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 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_2.json
+ 1
− 1
View file @ ad08a5d4
......@@ -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 } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_trace_pos_ensures.json
+ 1
− 1
View file @ ad08a5d4
......@@ -79,5 +79,5 @@
{ "Unfold 'EqS13_RealQuat_s'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 8.3262,
"time": 7.162,
"steps": 4632 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert.json
+ 3
− 3
View file @ ad08a5d4
......@@ -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.78 } ],
"verdict": "valid", "time": 1.06 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.14 } ],
"verdict": "valid", "time": 4. } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 3.91 } ],
"verdict": "valid", "time": 3.84 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_2.json
+ 3
− 3
View file @ ad08a5d4
......@@ -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.49 } ],
"verdict": "valid", "time": 3.34 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.86 } ],
"verdict": "valid", "time": 6.26 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.86 } ],
"verdict": "valid", "time": 5.88 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_3.json
+ 8
− 39
View file @ ad08a5d4
[ { "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. },
{ "prover": "script", "verdict": "valid" },
{ "header": "Definition", "tactic": "Wp.unfold", "params": {},
[ { "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_'": [ { "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": "Separated",
"children": { "Unfold 'P_unary_quaternion_1_'": [ { "header": "Separated",
"tactic": "Wp.separated",
"params": {},
"select": { "select": "inside-step",
......@@ -37,23 +12,17 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 2.26 } ],
"time": 2.3 } ],
"OnLeft":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 6.48 } ],
"time": 5.51 } ],
"OnRight":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 6.5 } ],
"time": 4.29 } ],
"OverLap":
[ { "prover": "qed",
"verdict": "valid" } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_4.json
+ 3
− 3
View file @ ad08a5d4
......@@ -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.47 } ],
"verdict": "valid", "time": 5.62 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 9.26 } ],
"verdict": "valid", "time": 11.86 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 9.52 } ],
"verdict": "valid", "time": 9.64 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures.json
+ 61
− 4
View file @ ad08a5d4
[ { "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.4 } ] } } ] } } ]
[ { "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" } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures_2.json
+ 6
− 6
View file @ ad08a5d4
......@@ -72,7 +72,7 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.58 } ] } } ],
"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.7821,
"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.01 } ] } } ],
"time": 1.22 } ] } } ],
"Goal 4/6":
[ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -121,7 +121,7 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.5 } ] } } ],
"time": 1.85 } ] } } ],
"Goal 5/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": 1.83 } ] } } ],
"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.2867,
"time": 2.664,
"steps": 28 },
{ "header": "Definition",
"tactic": "Wp.unfold",
......
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures_3.json
+ 1
− 1
View file @ ad08a5d4
......@@ -33,5 +33,5 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 3.0657,
"time": 3.2164,
"steps": 28 } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/lemma_quat_of_rmat_ortho.json
+ 2
− 2
View file @ ad08a5d4
......@@ -63,5 +63,5 @@
{ "Unfold 'EqS12_RealRMat_s'":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.03,
"steps": 45566 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 0.04,
"steps": 46240 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/math/pprz_algebra_float_convert_rmat_frama_c.h
+ 7
− 0
View file @ ad08a5d4
......@@ -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
* *****************************/
......
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