Skip to content

GitLab

Commit aa6dd827 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Update RTE verificatio

parent 7778193e
Hide whitespace changes
Inline Side-by-side
Showing with 303 additions and 25 deletions
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
View file @ aa6dd827
......@@ -59,7 +59,7 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_27 rm_0)",
"target": "(L_trace_2_ Mf32_2 rm_0)",
"pattern": "L_trace_2_$Mf32$rm" },
"children":
{ "Unfold 'L_trace_2_'":
......@@ -71,7 +71,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_2 rm_0))",
"pattern": "L_trace_1_L_l_RMat_of_FloatRMat$Mf32" },
"children":
{ "Unfold 'L_trace_1_'":
......@@ -83,7 +83,7 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_27 rm_0)",
"target": "(L_l_RMat_of_FloatRMat Mf32_2 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
......
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
View file @ aa6dd827
......@@ -59,7 +59,7 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_27 rm_0)",
"target": "(L_trace_2_ Mf32_2 rm_0)",
"pattern": "L_trace_2_$Mf32$rm" },
"children":
{ "Unfold 'L_trace_2_'":
......@@ -71,7 +71,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_2 rm_0))",
"pattern": "L_trace_1_L_l_RMat_of_FloatRMat$Mf32" },
"children":
{ "Unfold 'L_trace_1_'":
......@@ -83,7 +83,7 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_27 rm_0)",
"target": "(L_l_RMat_of_FloatRMat Mf32_2 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
......
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
View file @ aa6dd827
......@@ -20,7 +20,7 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_27 rm_0)",
"target": "(L_trace_2_ Mf32_2 rm_0)",
"pattern": "L_trace_2_$Mf32$rm" },
"children":
{ "Unfold 'L_trace_2_'":
......@@ -32,11 +32,74 @@
"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_2 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-goal",
"occur": 0,
"target": "(L_l_Quat_of_FloatQuat Mf32_0 q_0)",
"pattern": "L_l_Quat_of_FloatQuat$Mf32$q" },
"children":
{ "Unfold 'L_l_Quat_of_FloatQuat'":
[ { "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_l_FloatQuat_of_RMat_2_max_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_l_FloatQuat_of_RMat_2_max_1_{RealRMat_s}" },
"children":
{ "Unfold 'L_l_FloatQuat_of_RMat_2_max_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 (\\sqrt\n (1+a_0.F9_RealRMat_s_a22-a_0.F9_RealRMat_s_a00-a_0.F9_RealRMat_s_a11)) in\nlet r_1 = (2*r_0) in\n(EqS10_RealQuat_s\n {\n F10_RealQuat_s_qi =\n (a_0.F9_RealRMat_s_a01-a_0.F9_RealRMat_s_a10) div r_1 ;\n F10_RealQuat_s_qx =\n (a_0.F9_RealRMat_s_a02+a_0.F9_RealRMat_s_a20) div r_1 ;\n F10_RealQuat_s_qy =\n (a_0.F9_RealRMat_s_a12+a_0.F9_RealRMat_s_a21) div r_1 ;\n F10_RealQuat_s_qz = 1/2*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": "Split",
"tactic": "Wp.split",
"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 8)]-Mf32_0[(shift_float32 a_0 0)]-\n Mf32_0[(shift_float32 a_0 4)])) in\nlet r_1 = (2*r_0) in\n(Mf32_0[(shiftfield_F4_FloatQuat_qz q_0)]=(1/2*r_0))\n/\\ (Mf32_0[(shiftfield_F4_FloatQuat_qi q_0)]=\n ((Mf32_0[(shift_float32 a_0 1)]-Mf32_0[(shift_float32 a_0 3)]) div r_1))\n/\\ (Mf32_0[(shiftfield_F4_FloatQuat_qx q_0)]=\n ((Mf32_0[(shift_float32 a_0 2)]+Mf32_0[(shift_float32 a_0 6)]) div r_1))\n/\\ (Mf32_0[(shiftfield_F4_FloatQuat_qy q_0)]=\n ((Mf32_0[(shift_float32 a_0 5)]+Mf32_0[(shift_float32 a_0 7)]) div r_1))",
"pattern": "&====[]*[]/[]/[]/$Mf32shiftfield_F4_FloatQuat_qz" },
"children":
{ "Goal 1/4":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.569,
"steps": 357 } ],
"Goal 2/4":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.7146,
"steps": 380 } ],
"Goal 3/4":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.8463,
"steps": 379 } ],
"Goal 4/4":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 11.0712,
"steps": 814 } ] } } ] } } ] } } ] } } ]
"time": 2.7158,
"steps": 379 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert.json 0 → 100644
View file @ aa6dd827
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 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",
"params": {},
"select": { "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n(P_rotation_matrix\n {\n F9_RealRMat_s_a00 = Mf32_6[(shift_float32 a_0 0)] ;\n F9_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;\n F9_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;\n F9_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;\n F9_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;\n F9_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;\n F9_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;\n F9_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;\n F9_RealRMat_s_a22 = Mf32_6[(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_F6_FloatRMat_m rm_0) in\n(L_transpose\n {\n F9_RealRMat_s_a00 = Mf32_6[(shift_float32 a_0 0)] ;\n F9_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;\n F9_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;\n F9_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;\n F9_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;\n F9_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;\n F9_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;\n F9_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;\n F9_RealRMat_s_a22 = Mf32_6[(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_F6_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 F9_RealRMat_s_a00 = r_0 ;\n F9_RealRMat_s_a01 = r_1 ;\n F9_RealRMat_s_a02 = r_2 ;\n F9_RealRMat_s_a10 = r_3 ;\n F9_RealRMat_s_a11 = r_4 ;\n F9_RealRMat_s_a12 = r_5 ;\n F9_RealRMat_s_a20 = r_6 ;\n F9_RealRMat_s_a21 = r_7 ;\n F9_RealRMat_s_a22 = r_8\n }\n {\n F9_RealRMat_s_a00 = r_0 ;\n F9_RealRMat_s_a01 = r_3 ;\n F9_RealRMat_s_a02 = r_6 ;\n F9_RealRMat_s_a10 = r_1 ;\n F9_RealRMat_s_a11 = r_4 ;\n F9_RealRMat_s_a12 = r_7 ;\n F9_RealRMat_s_a20 = r_2 ;\n F9_RealRMat_s_a21 = r_5 ;\n F9_RealRMat_s_a22 = r_8\n })",
"pattern": "L_mult_RealRMat{RealRMat_s}{RealRMat_s}" },
"children":
{ "Unfold 'L_mult_RealRMat'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F6_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 = ((r_0*r_3)+(r_1*r_4)+(r_2*r_5)) in\nlet r_7 = Mf32_6[(shift_float32 a_0 6)] in\nlet r_8 = Mf32_6[(shift_float32 a_0 7)] in\nlet r_9 = Mf32_6[(shift_float32 a_0 8)] in\nlet r_10 = ((r_0*r_7)+(r_1*r_8)+(r_2*r_9)) in\nlet r_11 = ((r_3*r_7)+(r_4*r_8)+(r_5*r_9)) in\n(EqS9_RealRMat_s\n {\n F9_RealRMat_s_a00 = (r_0*r_0)+(r_1*r_1)+(r_2*r_2) ;\n F9_RealRMat_s_a01 = r_6 ;\n F9_RealRMat_s_a02 = r_10 ;\n F9_RealRMat_s_a10 = r_6 ;\n F9_RealRMat_s_a11 = (r_3*r_3)+(r_4*r_4)+(r_5*r_5) ;\n F9_RealRMat_s_a12 = r_11 ;\n F9_RealRMat_s_a20 = r_10 ;\n F9_RealRMat_s_a21 = r_11 ;\n F9_RealRMat_s_a22 = (r_7*r_7)+(r_8*r_8)+(r_9*r_9)\n } L_id_rmat)",
"pattern": "EqS9_RealRMat_s{RealRMat_s}L_id_rmat" },
"children":
{ "Unfold 'EqS9_RealRMat_s'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "L_id_rmat",
"pattern": "L_id_rmat" },
"children":
{ "Unfold 'L_id_rmat'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 0.54 } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_10.json 0 → 100644
View file @ aa6dd827
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_11.json 0 → 100644
View file @ aa6dd827
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
sw/airborne/.frama-c/wp/script/int32_quat_vmult_assert_rte_signed_overflow_49.json → sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_12.json
View file @ aa6dd827
[ { "prover": "Z3:4.8.10:counterexamples", "verdict": "failed" },
[ { "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": "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 0 → 100644
View file @ aa6dd827
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 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",
"params": {},
"select": { "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n(P_rotation_matrix\n {\n F9_RealRMat_s_a00 = Mf32_6[(shift_float32 a_0 0)] ;\n F9_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;\n F9_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;\n F9_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;\n F9_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;\n F9_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;\n F9_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;\n F9_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;\n F9_RealRMat_s_a22 = Mf32_6[(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_F6_FloatRMat_m rm_0) in\n(L_transpose\n {\n F9_RealRMat_s_a00 = Mf32_6[(shift_float32 a_0 0)] ;\n F9_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;\n F9_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;\n F9_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;\n F9_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;\n F9_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;\n F9_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;\n F9_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;\n F9_RealRMat_s_a22 = Mf32_6[(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": "L_id_rmat",
"pattern": "L_id_rmat" },
"children":
{ "Unfold 'L_id_rmat'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F6_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 F9_RealRMat_s_a00 = r_0 ;\n F9_RealRMat_s_a01 = r_1 ;\n F9_RealRMat_s_a02 = r_2 ;\n F9_RealRMat_s_a10 = r_3 ;\n F9_RealRMat_s_a11 = r_4 ;\n F9_RealRMat_s_a12 = r_5 ;\n F9_RealRMat_s_a20 = r_6 ;\n F9_RealRMat_s_a21 = r_7 ;\n F9_RealRMat_s_a22 = r_8\n }\n {\n F9_RealRMat_s_a00 = r_0 ;\n F9_RealRMat_s_a01 = r_3 ;\n F9_RealRMat_s_a02 = r_6 ;\n F9_RealRMat_s_a10 = r_1 ;\n F9_RealRMat_s_a11 = r_4 ;\n F9_RealRMat_s_a12 = r_7 ;\n F9_RealRMat_s_a20 = r_2 ;\n F9_RealRMat_s_a21 = r_5 ;\n F9_RealRMat_s_a22 = r_8\n })",
"pattern": "L_mult_RealRMat{RealRMat_s}{RealRMat_s}" },
"children":
{ "Unfold 'L_mult_RealRMat'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F6_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 = ((r_0*r_3)+(r_1*r_4)+(r_2*r_5)) in\nlet r_7 = Mf32_6[(shift_float32 a_0 6)] in\nlet r_8 = Mf32_6[(shift_float32 a_0 7)] in\nlet r_9 = Mf32_6[(shift_float32 a_0 8)] in\nlet r_10 = ((r_0*r_7)+(r_1*r_8)+(r_2*r_9)) in\nlet r_11 = ((r_3*r_7)+(r_4*r_8)+(r_5*r_9)) in\n(EqS9_RealRMat_s\n {\n F9_RealRMat_s_a00 = (r_0*r_0)+(r_1*r_1)+(r_2*r_2) ;\n F9_RealRMat_s_a01 = r_6 ;\n F9_RealRMat_s_a02 = r_10 ;\n F9_RealRMat_s_a10 = r_6 ;\n F9_RealRMat_s_a11 = (r_3*r_3)+(r_4*r_4)+(r_5*r_5) ;\n F9_RealRMat_s_a12 = r_11 ;\n F9_RealRMat_s_a20 = r_10 ;\n F9_RealRMat_s_a21 = r_11 ;\n F9_RealRMat_s_a22 = (r_7*r_7)+(r_8*r_8)+(r_9*r_9)\n }\n {\n F9_RealRMat_s_a00 = 1 ;\n F9_RealRMat_s_a01 = 0 ;\n F9_RealRMat_s_a02 = 0 ;\n F9_RealRMat_s_a10 = 0 ;\n F9_RealRMat_s_a11 = 1 ;\n F9_RealRMat_s_a12 = 0 ;\n F9_RealRMat_s_a20 = 0 ;\n F9_RealRMat_s_a21 = 0 ;\n F9_RealRMat_s_a22 = 1\n })",
"pattern": "EqS9_RealRMat_s{RealRMat_s}{RealRMat_s}" },
"children":
{ "Unfold 'EqS9_RealRMat_s'":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 1.57,
"steps": 3136482 } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_3.json 0 → 100644
View file @ aa6dd827
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_4.json 0 → 100644
View file @ aa6dd827
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_5.json 0 → 100644
View file @ aa6dd827
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_6.json 0 → 100644
View file @ aa6dd827
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_7.json 0 → 100644
View file @ aa6dd827
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_8.json 0 → 100644
View file @ aa6dd827
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_9.json 0 → 100644
View file @ aa6dd827
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_trace_pos_ensures.json
View file @ aa6dd827
......@@ -69,11 +69,35 @@
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_27 rm_0)",
"target": "(L_trace_2_ Mf32_2 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_2 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_2 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": 13.5863,
"steps": 3572 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 4.8543,
"steps": 1495 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert.json
View file @ aa6dd827
......@@ -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.68 } ],
"verdict": "valid", "time": 1. } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 3.67 } ],
"verdict": "valid", "time": 4.45 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 3.55 } ],
"verdict": "valid", "time": 4.22 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_2.json
View file @ aa6dd827
......@@ -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.02 } ],
"verdict": "valid", "time": 3.39 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.17 } ],
"verdict": "valid", "time": 4.36 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.15 } ],
"verdict": "valid", "time": 4.51 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_3.json
View file @ aa6dd827
......@@ -3,7 +3,7 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 8.8322,
"verdict": "valid", "time": 7.2054,
"steps": 114 } ],
"OnLeft": [ { "header": "Definition",
"tactic": "Wp.unfold", "params": {},
......@@ -15,7 +15,7 @@
"children": { "Unfold 'P_unary_quaterion'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 5.6 } ] } } ],
"time": 5.2 } ] } } ],
"OnRight": [ { "header": "Definition",
"tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step",
......@@ -26,5 +26,5 @@
"children": { "Unfold 'P_unary_quaterion'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 5.76 } ] } } ],
"time": 5.2 } ] } } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_4.json
View file @ aa6dd827
......@@ -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.75 } ],
"verdict": "valid", "time": 4.79 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 12.59 } ],
"verdict": "valid", "time": 10.18 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 11.58 } ],
"verdict": "valid", "time": 9.67 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
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