Skip to content

GitLab

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

Merge wp script

parents 94a3e9a2 cf07e71a
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 2560 additions and 205 deletions
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
View file @ b4501f19
......@@ -89,5 +89,5 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.2313,
"steps": 989 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 1.4631,
"steps": 992 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
View file @ b4501f19
......@@ -36,5 +36,5 @@
{ "Unfold 'L_trace_2_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.5689,
"steps": 1249 } ] } } ] } } ] } } ] } } ]
"time": 2.9531,
"steps": 1252 } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
View file @ b4501f19
......@@ -58,8 +58,8 @@
{ "Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.839,
"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
View file @ b4501f19
......@@ -49,8 +49,8 @@
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.3,
"steps": 429570 } ],
"time": 0.31,
"steps": 431175 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
......@@ -76,8 +76,8 @@
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.29,
"steps": 394374 } ],
"time": 0.33,
"steps": 395604 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
......@@ -92,13 +92,13 @@
{ "Then":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.04,
"steps": 207345 } ],
"time": 0.05,
"steps": 223243 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.29,
"steps": 393035 } ] } } ] } } ],
"time": 0.4,
"steps": 394729 } ] } } ] } } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
......@@ -113,10 +113,10 @@
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.31,
"steps": 393824 } ],
"time": 0.32,
"steps": 395218 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.31,
"steps": 390520 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 0.34,
"steps": 392197 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_2.json
View file @ b4501f19
......@@ -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": 4.7984,
"steps": 1623 } ] } } ]
"verdict": "valid", "time": 5.4931,
"steps": 1628 } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_trace_pos_ensures.json
View file @ b4501f19
......@@ -79,5 +79,5 @@
{ "Unfold 'EqS13_RealQuat_s'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 7.3419,
"steps": 4599 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 8.3262,
"steps": 4632 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_312_ensures.json
View file @ b4501f19
......@@ -59,30 +59,30 @@
{ "Goal 1/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.2916,
"time": 1.2917,
"steps": 102 } ],
"Goal 2/6":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.04,
"steps": 65603 } ],
"steps": 69389 } ],
"Goal 3/6":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.03,
"steps": 65611 } ],
"steps": 69395 } ],
"Goal 4/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.8936,
"time": 1.9416,
"steps": 102 } ],
"Goal 5/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.6318,
"time": 1.6413,
"steps": 102 } ],
"Goal 6/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.4294,
"time": 1.4217,
"steps": 102 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_312_ensures_2.json
View file @ b4501f19
......@@ -11,5 +11,5 @@
"children": { "Unfold 'P_special_orthogonal'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.6138,
"time": 1.6817,
"steps": 102 } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_321_ensures.json
View file @ b4501f19
......@@ -59,30 +59,30 @@
{ "Goal 1/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.2828,
"time": 1.4375,
"steps": 102 } ],
"Goal 2/6":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.44,
"steps": 2395621 } ],
"time": 0.66,
"steps": 2414090 } ],
"Goal 3/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.7804,
"time": 2.4657,
"steps": 102 } ],
"Goal 4/6":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.48,
"steps": 2395606 } ],
"time": 0.56,
"steps": 2414075 } ],
"Goal 5/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.3651,
"time": 2.2324,
"steps": 102 } ],
"Goal 6/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.3739,
"time": 2.0371,
"steps": 102 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_321_ensures_2.json
View file @ b4501f19
......@@ -11,5 +11,5 @@
"children": { "Unfold 'P_special_orthogonal'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.5048,
"time": 2.1125,
"steps": 102 } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert.json
View file @ b4501f19
......@@ -5,7 +5,7 @@
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 0.89 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.11 } ],
"verdict": "valid", "time": 4.23 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 3.95 } ],
"verdict": "valid", "time": 4.18 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_2.json
View file @ b4501f19
......@@ -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.69 } ],
"verdict": "valid", "time": 3.64 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.26 } ],
"verdict": "valid", "time": 5.3 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.07 } ],
"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
View file @ 94a3e9a2
[ { "prover": "script", "verdict": "valid" },
{ "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": "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": 2,
"kind": "have",
"occur": 0,
"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": 9.6 } ],
"OverLap":
[ { "prover": "qed",
"verdict": "valid" } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_4.json
View file @ b4501f19
......@@ -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.61 } ],
"verdict": "valid", "time": 5.8 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 10.26 } ],
"verdict": "valid", "time": 8.96 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 9.91 } ],
"verdict": "valid", "time": 8.91 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures.json
View file @ b4501f19
......@@ -12,4 +12,4 @@
"children": { "Unfold 'L_l_RMat_of_FloatQuat_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 3.07 } ] } } ] } } ]
"time": 3.24 } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures_2.json
View file @ b4501f19
......@@ -72,12 +72,24 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 2. } ] } } ],
"time": 1.48 } ] } } ],
"Goal 2/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": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 9.6615,
"steps": 134 } ],
"time": 1.7839,
"steps": 28 } ] } } ],
"Goal 3/6":
[ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -93,13 +105,9 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.29 } ] } } ],
"time": 1.07 } ] } } ],
"Goal 4/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 10.8366,
"steps": 138 },
{ "header": "Definition",
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
......@@ -107,20 +115,29 @@
"at": 2,
"kind": "have",
"occur": 0,
"target": "(P_unary_quaternion Mf32_1 q_0)",
"pattern": "P_unary_quaternion$Mf32$q" },
"target": "(P_unary_quaternion_1_ Mf32_1 q_0)",
"pattern": "P_unary_quaternion_1_$Mf32$q" },
"children":
{ "Unfold 'P_unary_quaternion'":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.37 } ] } } ],
"time": 1.85 } ] } } ],
"Goal 5/6":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "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": 12.4057,
"steps": 138 } ],
"time": 2.18 } ] } } ],
"Goal 6/6":
[ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -136,5 +153,22 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.6674,
"steps": 28 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 2.5372,
"steps": 28 },
{ "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": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.43 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
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