Skip to content

GitLab

Commit 94a3e9a2 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Merge wp script

parents d503e723 df02b4a5
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1021 additions and 114 deletions
sw/airborne/.frama-c/wp/interactive/lemma_impl_rmat_quat.v 0 → 100644
View file @ 94a3e9a2
This diff is collapsed.
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
View file @ 94a3e9a2
......@@ -89,5 +89,5 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.404,
"time": 1.2313,
"steps": 989 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
View file @ 94a3e9a2
......@@ -36,5 +36,5 @@
{ "Unfold 'L_trace_2_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.5856,
"time": 2.5689,
"steps": 1249 } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
View file @ 94a3e9a2
......@@ -58,7 +58,7 @@
{ "Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.8028,
"time": 1.839,
"steps": 1008 },
{ "header": "Definition",
"tactic": "Wp.unfold",
......
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
View file @ 94a3e9a2
......@@ -49,8 +49,8 @@
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.29,
"steps": 426627 } ],
"time": 0.3,
"steps": 429570 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
......@@ -76,8 +76,8 @@
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.33,
"steps": 389571 } ],
"time": 0.29,
"steps": 394374 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
......@@ -93,12 +93,12 @@
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.04,
"steps": 202708 } ],
"steps": 207345 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.35,
"steps": 387857 } ] } } ] } } ],
"time": 0.29,
"steps": 393035 } ] } } ] } } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
......@@ -113,10 +113,10 @@
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.29,
"steps": 382945 } ],
"time": 0.31,
"steps": 393824 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.51,
"steps": 385200 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 0.31,
"steps": 390520 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_2.json
View file @ 94a3e9a2
[ { "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.8391, "steps": 722 } ],
"Else": [ { "prover": "Alt-Ergo:2.3.3", "verdict": "valid",
"time": 4.943, "steps": 1331 } ] } } ]
[ { "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": 4.7984,
"steps": 1623 } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_trace_pos_ensures.json
View file @ 94a3e9a2
......@@ -79,5 +79,5 @@
{ "Unfold 'EqS13_RealQuat_s'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 9.2362,
"time": 7.3419,
"steps": 4599 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_312_ensures.json
View file @ 94a3e9a2
......@@ -59,30 +59,30 @@
{ "Goal 1/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.3726,
"time": 1.2916,
"steps": 102 } ],
"Goal 2/6":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.03,
"steps": 63835 } ],
"time": 0.04,
"steps": 65603 } ],
"Goal 3/6":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.04,
"steps": 63843 } ],
"time": 0.03,
"steps": 65611 } ],
"Goal 4/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.1605,
"time": 1.8936,
"steps": 102 } ],
"Goal 5/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.0736,
"time": 1.6318,
"steps": 102 } ],
"Goal 6/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.5461,
"time": 1.4294,
"steps": 102 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_312_ensures_2.json
View file @ 94a3e9a2
......@@ -11,5 +11,5 @@
"children": { "Unfold 'P_special_orthogonal'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.8898,
"time": 1.6138,
"steps": 102 } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_321_ensures.json
View file @ 94a3e9a2
......@@ -59,30 +59,30 @@
{ "Goal 1/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.275,
"time": 1.2828,
"steps": 102 } ],
"Goal 2/6":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.49,
"steps": 2378344 } ],
"time": 0.44,
"steps": 2395621 } ],
"Goal 3/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.0891,
"time": 1.7804,
"steps": 102 } ],
"Goal 4/6":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.57,
"steps": 2378309 } ],
"time": 0.48,
"steps": 2395606 } ],
"Goal 5/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.6148,
"time": 1.3651,
"steps": 102 } ],
"Goal 6/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.5453,
"time": 1.3739,
"steps": 102 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_321_ensures_2.json
View file @ 94a3e9a2
......@@ -11,5 +11,5 @@
"children": { "Unfold 'P_special_orthogonal'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.8685,
"time": 1.5048,
"steps": 102 } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert.json
View file @ 94a3e9a2
......@@ -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": 1.06 } ],
"verdict": "valid", "time": 0.89 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.67 } ],
"verdict": "valid", "time": 4.11 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.03 } ],
"verdict": "valid", "time": 3.95 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_2.json
View file @ 94a3e9a2
......@@ -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.84 } ],
"verdict": "valid", "time": 3.69 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.31 } ],
"verdict": "valid", "time": 5.26 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.69 } ],
"verdict": "valid", "time": 5.07 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_3.json
View file @ 94a3e9a2
[ { "header": "Separated", "tactic": "Wp.separated", "params": {},
[ { "prover": "script", "verdict": "valid" },
{ "header": "Definition", "tactic": "Wp.unfold", "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": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 12.7988,
"steps": 130 } ],
"OnLeft": [ { "header": "Validity Range",
"tactic": "Wp.valid", "params": {},
"select": { "select": "inside-step",
"at": 3, "kind": "have",
"occur": 0,
"target": "(valid_rd Malloc_0 q_0 4)",
"pattern": "valid_rd$Malloc$q4" },
"children": { "Valid (Read)": [ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
"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": "Validity Range",
"tactic": "Wp.valid",
"params": {},
"select": { "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "(valid_rd Malloc_0 q_0 4)",
"pattern": "valid_rd$Malloc$q4" },
"children": { "Valid (Read)":
[ { "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": "Validity Range",
"tactic": "Wp.valid",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "(valid_rw Malloc_0 rm_0 9)",
"pattern": "valid_rw$Malloc$rm9" },
"children":
{ "Valid (Read & Write)":
[ { "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": "(shiftfield_F7_FloatQuat_qy q_0)",
"pattern": "shiftfield_F7_FloatQuat_qy$q" },
"children":
{ "Unfold 'shiftfield_F7_FloatQuat_qy'":
[ { "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",
"tactic": "Wp.separated",
"params": {},
"select":
{ "select": "inside-step",
"at": 3,
"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": "CVC4:1.9-prerelease:strings+counterexamples",
"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",
"verdict": "valid",
"time": 2.63 } ],
"OnLeft":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 8.29 } ],
"OnRight":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 5.19 } ] } } ] } } ],
"OnRight": [ { "header": "Definition",
"tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step",
"at": 3, "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": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 5.8 } ] } } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
"time": 9.6 } ],
"OverLap":
[ { "prover": "qed",
"verdict": "valid" } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_4.json
View file @ 94a3e9a2
......@@ -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.43 } ],
"verdict": "valid", "time": 5.61 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 10.54 } ],
"verdict": "valid", "time": 10.26 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 10.16 } ],
"verdict": "valid", "time": 9.91 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures.json
View file @ 94a3e9a2
......@@ -10,26 +10,6 @@
"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_'":
[ { "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'":
[ { "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": 101737 } ] } } ] } } ] } } ] } } ]
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 3.07 } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures_2.json
View file @ 94a3e9a2
......@@ -49,6 +49,79 @@
"pattern": "L_l_RMat_of_FloatRMat[=]$rm[=]shift_float32" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-goal",
"target": "let r_0 = Mf32_1[(shiftfield_F7_FloatQuat_qi q_0)] in\nlet r_1 = Mf32_1[(shiftfield_F7_FloatQuat_qx q_0)] in\nlet r_2 = (2*r_0*r_1) in\nlet r_3 = Mf32_1[(shiftfield_F7_FloatQuat_qy q_0)] in\nlet r_4 = Mf32_1[(shiftfield_F7_FloatQuat_qz q_0)] in\nlet r_5 = (2*r_3*r_4) in\nlet r_6 = (r_2+r_5) in\nlet r_7 = (2*r_0*r_0) in\nlet r_8 = (r_7+(2*r_3*r_3)-1) in\nlet r_9 = (2*r_0*r_4) in\nlet r_10 = (2*r_1*r_3) in\nlet r_11 = (r_10-r_9) in\nlet r_12 = (2*r_0*r_3) in\nlet r_13 = (2*r_1*r_4) in\nlet r_14 = (r_12+r_13) in\nlet r_15 = (r_7+(2*r_4*r_4)-1) in\nlet r_16 = (r_5-r_2) in\nlet r_17 = (r_9+r_10) in\nlet r_18 = (r_7+(2*r_1*r_1)-1) in\nlet r_19 = (r_13-r_12) in\n(((r_6*r_6)+(r_8*r_8)+(r_11*r_11))=1)\n/\\ (((r_14*r_14)+(r_15*r_15)+(r_16*r_16))=1)\n/\\ (((r_17*r_17)+(r_18*r_18)+(r_19*r_19))=1)\n/\\ (((r_6*r_15)+(r_14*r_11)+(r_8*r_16))=0)\n/\\ (((r_6*r_19)+(r_17*r_8)+(r_18*r_11))=0)\n/\\ (((r_14*r_18)+(r_17*r_16)+(r_15*r_19))=0)",
"pattern": "&======+1+1+1+0+0+0*************" },
"children":
{ "Goal 1/6":
[ { "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": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 2. } ] } } ],
"Goal 2/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 9.6615,
"steps": 134 } ],
"Goal 3/6":
[ { "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": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.29 } ] } } ],
"Goal 4/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 10.8366,
"steps": 138 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "(P_unary_quaternion Mf32_1 q_0)",
"pattern": "P_unary_quaternion$Mf32$q" },
"children":
{ "Unfold 'P_unary_quaternion'":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.37 } ] } } ],
"Goal 5/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 12.4057,
"steps": 138 } ],
"Goal 6/6":
[ { "header": "Definition",