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

Merging origin/master

parents 98300a48 b4501f19
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 183 additions and 175 deletions
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
+ 2
− 2
View file @ e67a1d30
......@@ -89,5 +89,5 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.5505,
"steps": 989 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 1.4631,
"steps": 992 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
+ 2
− 2
View file @ e67a1d30
......@@ -36,5 +36,5 @@
{ "Unfold 'L_trace_2_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.7065,
"steps": 1249 } ] } } ] } } ] } } ] } } ]
"time": 2.9531,
"steps": 1252 } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
+ 2
− 2
View file @ e67a1d30
......@@ -58,8 +58,8 @@
{ "Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.4316,
"steps": 1008 },
"time": 2.4767,
"steps": 1013 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
......
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
+ 122
− 9
View file @ e67a1d30
[ { "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": "Z3:4.8.6:counterexamples",
"verdict": "valid", "time": 0.31,
"steps": 404607 } ],
"Else": [ { "prover": "Alt-Ergo:2.3.3", "verdict": "valid",
"time": 3.7782, "steps": 1331 } ] } } ]
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 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'": [ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select": { "select": "inside-step",
"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_1[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_1[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_1[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_1[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_1[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_1[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_1[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_1[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_1[(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_F9_FloatRMat_m rm_0) in\n(L_transpose\n {\n F12_RealRMat_s_a00 = Mf32_1[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_1[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_1[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_1[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_1[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_1[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_1[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_1[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_1[(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_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_1[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_1[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_1[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_1[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_1[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_1[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_1[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_1[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_1[(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'":
[ { "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": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.31,
"steps": 431175 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 10,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nMf32_1[(shift_float32 a_0 4)]<Mf32_1[(shift_float32 a_0 0)]",
"pattern": "<[][]$Mf32shift_float32$Mf32shift_float32" },
"children":
{ "Then":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 12,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nMf32_1[(shift_float32 a_0 8)]<Mf32_1[(shift_float32 a_0 0)]",
"pattern": "<[][]$Mf32shift_float32$Mf32shift_float32" },
"children":
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.33,
"steps": 395604 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 16,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nMf32_1[(shift_float32 a_0 8)]<Mf32_1[(shift_float32 a_0 4)]",
"pattern": "<[][]$Mf32shift_float32$Mf32shift_float32" },
"children":
{ "Then":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.05,
"steps": 223243 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.4,
"steps": 394729 } ] } } ] } } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 13,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nMf32_1[(shift_float32 a_0 8)]<Mf32_1[(shift_float32 a_0 4)]",
"pattern": "<[][]$Mf32shift_float32$Mf32shift_float32" },
"children":
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.32,
"steps": 395218 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.34,
"steps": 392197 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_2.json
+ 7
− 8
View file @ e67a1d30
[ { "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.7925, "steps": 722 } ],
"Else": [ { "prover": "Alt-Ergo:2.3.3", "verdict": "valid",
"time": 4.5395, "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": 5.4931,
"steps": 1628 } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_trace_pos_ensures.json
+ 2
− 2
View file @ e67a1d30
......@@ -79,5 +79,5 @@
{ "Unfold 'EqS13_RealQuat_s'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 9.5815,
"steps": 4599 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 8.3262,
"steps": 4632 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_312_ensures.json
+ 5
− 5
View file @ e67a1d30
......@@ -59,7 +59,7 @@
{ "Goal 1/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.419,
"time": 1.2917,
"steps": 102 } ],
"Goal 2/6":
[ { "prover": "Z3:4.8.6:counterexamples",
......@@ -69,20 +69,20 @@
"Goal 3/6":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.04,
"time": 0.03,
"steps": 69395 } ],
"Goal 4/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.5923,
"time": 1.9416,
"steps": 102 } ],
"Goal 5/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.0899,
"time": 1.6413,
"steps": 102 } ],
"Goal 6/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.8943,
"time": 1.4217,
"steps": 102 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_312_ensures_2.json
+ 1
− 1
View file @ e67a1d30
......@@ -11,5 +11,5 @@
"children": { "Unfold 'P_special_orthogonal'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.4431,
"time": 1.6817,
"steps": 102 } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_321_ensures.json
+ 6
− 6
View file @ e67a1d30
......@@ -59,30 +59,30 @@
{ "Goal 1/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.3571,
"time": 1.4375,
"steps": 102 } ],
"Goal 2/6":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.51,
"time": 0.66,
"steps": 2414090 } ],
"Goal 3/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.4556,
"time": 2.4657,
"steps": 102 } ],
"Goal 4/6":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.55,
"time": 0.56,
"steps": 2414075 } ],
"Goal 5/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.889,
"time": 2.2324,
"steps": 102 } ],
"Goal 6/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.9076,
"time": 2.0371,
"steps": 102 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_321_ensures_2.json
+ 1
− 1
View file @ e67a1d30
......@@ -11,5 +11,5 @@
"children": { "Unfold 'P_special_orthogonal'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.9546,
"time": 2.1125,
"steps": 102 } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert.json
+ 2
− 2
View file @ e67a1d30
......@@ -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.09 } ],
"verdict": "valid", "time": 0.89 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.23 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.53 } ],
"verdict": "valid", "time": 4.18 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_2.json
+ 3
− 3
View file @ e67a1d30
......@@ -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.6 } ],
"verdict": "valid", "time": 3.64 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 6.07 } ],
"verdict": "valid", "time": 5.3 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.57 } ],
"verdict": "valid", "time": 5.38 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_3.json deleted 100644 → 0
+ 0
− 30
View file @ 98300a48
[ { "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": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 12.7704,
"steps": 130 } ],
"OnLeft": [ { "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": 7.14 } ] } } ],
"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": 7.47 } ] } } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_4.json
+ 3
− 3
View file @ e67a1d30
......@@ -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.72 } ],
"verdict": "valid", "time": 5.8 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 10.1 } ],
"verdict": "valid", "time": 8.96 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 10.07 } ],
"verdict": "valid", "time": 8.91 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures.json
+ 1
− 1
View file @ e67a1d30
......@@ -12,4 +12,4 @@
"children": { "Unfold 'L_l_RMat_of_FloatQuat_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 3.42 } ] } } ] } } ]
"time": 3.24 } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures_2.json
+ 20
− 94
View file @ e67a1d30
[ { "prover": "script", "verdict": "valid" },
{ "header": "Definition", "tactic": "Wp.unfold", "params": {},
[ { "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\n(P_rotation_matrix\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": "P_rotation_matrixL_l_RMat_of_FloatRMat" },
......@@ -73,26 +72,9 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 2.52 } ] } } ],
"time": 1.48 } ] } } ],
"Goal 2/6":
[ { "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": 16. },
{ "header": "Definition",
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
......@@ -104,14 +86,9 @@
"pattern": "P_unary_quaternion_1_$Mf32$q" },
"children":
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.66 },
{ "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.5465,
"time": 1.7839,
"steps": 28 } ] } } ],
"Goal 3/6":
[ { "header": "Definition",
......@@ -128,26 +105,9 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.57 } ] } } ],
"time": 1.07 } ] } } ],
"Goal 4/6":
[ { "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": 15. },
{ "header": "Definition",
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
......@@ -159,30 +119,11 @@
"pattern": "P_unary_quaternion_1_$Mf32$q" },
"children":
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.4 } ] } } ],
"time": 1.85 } ] } } ],
"Goal 5/6":
[ { "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": 18. },
{ "header": "Definition",
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
......@@ -194,41 +135,26 @@
"pattern": "P_unary_quaternion_1_$Mf32$q" },
"children":
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.68 } ] } } ],
"time": 2.18 } ] } } ],
"Goal 6/6":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 36,
"at": 2,
"kind": "have",
"occur": 0,
"target": "(shift_float32 (shiftfield_F9_FloatRMat_m rm_0) 7)",
"pattern": "shift_float32shiftfield_F9_FloatRMat_m" },
"target": "(P_unary_quaternion_1_ Mf32_1 q_0)",
"pattern": "P_unary_quaternion_1_$Mf32$q" },
"children":
{ "Unfold 'shift_float32'":
[ { "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": 18. },
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.5372,
"steps": 28 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
......
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures_3.json
+ 1
− 1
View file @ e67a1d30
......@@ -33,5 +33,5 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 3.6903,
"time": 3.0835,
"steps": 28 } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/int32_mat_mul_assert_rte_mem_access_5.json
+ 1
− 1
View file @ e67a1d30
......@@ -4,4 +4,4 @@
"pattern": "P_rvalid_int_mat_3_$Malloc$Mptr[=]" },
"children": { "Unfold 'P_rvalid_int_mat_3_'": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 6.46 } ] } } ]
"time": 6.5 } ] } } ]
sw/airborne/.frama-c/wp/script/int32_mat_mul_assert_rte_mem_access_6.json
+ 1
− 1
View file @ e67a1d30
......@@ -4,5 +4,5 @@
"pattern": "P_rvalid_int_mat_3_$Malloc$Mptr[=]" },
"children": { "Unfold 'P_rvalid_int_mat_3_'": [ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.74,
"time": 0.81,
"steps": 2170940 } ] } } ]
sw/airborne/.frama-c/wp/script/int32_mat_mul_assert_rte_mem_access_7.json
+ 1
− 1
View file @ e67a1d30
......@@ -37,4 +37,4 @@
{ "Unfold 'P_rvalid_int_mat_2_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 2.6 } ] } } ] } } ] } } ] } } ]
"time": 2.75 } ] } } ] } } ] } } ] } } ]
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