Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Open sidebar
POLLIEN Baptiste
paparazzi-frama-c
Commits
364842fd
Commit
364842fd
authored
Apr 26, 2021
by
POLLIEN Baptiste
Browse files
Add special orthogonal postcondition
parent
19613b16
Changes
34
Hide whitespace changes
Inline
Side-by-side
Showing
20 changed files
with
120 additions
and
174 deletions
+120
-174
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
...frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
+47
-2
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
...frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
+3
-73
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
...frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
+2
-2
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
...irborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
+5
-5
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_11.json
...orne/.frama-c/wp/script/float_quat_of_rmat_assert_11.json
+6
-6
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_12.json
...orne/.frama-c/wp/script/float_quat_of_rmat_assert_12.json
+0
-8
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_13.json
...orne/.frama-c/wp/script/float_quat_of_rmat_assert_13.json
+6
-5
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_14.json
...orne/.frama-c/wp/script/float_quat_of_rmat_assert_14.json
+5
-16
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_15.json
...orne/.frama-c/wp/script/float_quat_of_rmat_assert_15.json
+0
-7
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_16.json
...orne/.frama-c/wp/script/float_quat_of_rmat_assert_16.json
+6
-6
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_17.json
...orne/.frama-c/wp/script/float_quat_of_rmat_assert_17.json
+5
-5
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_18.json
...orne/.frama-c/wp/script/float_quat_of_rmat_assert_18.json
+6
-6
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_19.json
...orne/.frama-c/wp/script/float_quat_of_rmat_assert_19.json
+6
-6
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_2.json
...borne/.frama-c/wp/script/float_quat_of_rmat_assert_2.json
+6
-6
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_20.json
...orne/.frama-c/wp/script/float_quat_of_rmat_assert_20.json
+6
-6
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_22.json
...orne/.frama-c/wp/script/float_quat_of_rmat_assert_22.json
+0
-2
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_24.json
...orne/.frama-c/wp/script/float_quat_of_rmat_assert_24.json
+0
-2
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_ensures.json
...rborne/.frama-c/wp/script/float_quat_of_rmat_ensures.json
+1
-1
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_trace_pos_ensures.json
...ama-c/wp/script/float_quat_of_rmat_trace_pos_ensures.json
+2
-2
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_312_ensures.json
.../.frama-c/wp/script/float_rmat_of_eulers_312_ensures.json
+8
-8
No files found.
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
View file @
364842fd
...
...
@@ -42,7 +42,52 @@
"pattern"
:
"L_l_Quat_of_FloatQuat$Mf32$q"
},
"children"
:
{
"Unfold 'L_l_Quat_of_FloatQuat'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-goal"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 =
\n
(
\\
sqrt
\n
(1+Mf32_0[(shift_float32 a_0 0)]-Mf32_0[(shift_float32 a_0 4)]-
\n
Mf32_0[(shift_float32 a_0 8)])) in
\n
let r_1 = (2*r_0) in
\n
(EqS13_RealQuat_s
\n
{
\n
F13_RealQuat_s_qi =
\n
(Mf32_0[(shift_float32 a_0 5)]-Mf32_0[(shift_float32 a_0 7)]) div r_1 ;
\n
F13_RealQuat_s_qx = 1/2*r_0 ;
\n
F13_RealQuat_s_qy =
\n
(Mf32_0[(shift_float32 a_0 1)]+Mf32_0[(shift_float32 a_0 3)]) div r_1 ;
\n
F13_RealQuat_s_qz =
\n
(Mf32_0[(shift_float32 a_0 2)]+Mf32_0[(shift_float32 a_0 6)]) div r_1
\n
}
\n
{
\n
F13_RealQuat_s_qi = Mf32_0[(shiftfield_F7_FloatQuat_qi q_0)] ;
\n
F13_RealQuat_s_qx = Mf32_0[(shiftfield_F7_FloatQuat_qx q_0)] ;
\n
F13_RealQuat_s_qy = Mf32_0[(shiftfield_F7_FloatQuat_qy q_0)] ;
\n
F13_RealQuat_s_qz = Mf32_0[(shiftfield_F7_FloatQuat_qz q_0)]
\n
})"
,
"pattern"
:
"EqS13_RealQuat_s{RealQuat_s}{RealQuat_s}"
},
"children"
:
{
"Unfold 'EqS13_RealQuat_s'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
3
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_trace_2_ Mf32_1 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_1 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_1 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"
:
1
1.8791
,
"steps"
:
1715
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
"time"
:
1
.148
,
"steps"
:
974
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
View file @
364842fd
...
...
@@ -22,52 +22,6 @@
"pattern"
:
"L_l_FloatQuat_of_RMat_1_max_1_{RealRMat_s}"
},
"children"
:
{
"Unfold 'L_l_FloatQuat_of_RMat_1_max_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"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-goal"
,
"target"
:
"let a_0 = (L_l_RMat_of_FloatRMat Mf32_0 rm_0) in
\n
let r_0 =
\n
(
\\
sqrt
\n
(1+a_0.F9_RealRMat_s_a11-a_0.F9_RealRMat_s_a00-a_0.F9_RealRMat_s_a22)) in
\n
let r_1 = (2*r_0) in
\n
(EqS10_RealQuat_s
\n
{
\n
F10_RealQuat_s_qi =
\n
(a_0.F9_RealRMat_s_a20-a_0.F9_RealRMat_s_a02) div r_1 ;
\n
F10_RealQuat_s_qx =
\n
(a_0.F9_RealRMat_s_a01+a_0.F9_RealRMat_s_a10) div r_1 ;
\n
F10_RealQuat_s_qy = 1/2*r_0 ;
\n
F10_RealQuat_s_qz =
\n
(a_0.F9_RealRMat_s_a12+a_0.F9_RealRMat_s_a21) div r_1
\n
} (L_l_Quat_of_FloatQuat Mf32_0 q_0))"
,
"pattern"
:
"EqS10_RealQuat_s{RealQuat_s}L_l_Quat_of_FloatQuat"
},
"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"
:
"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"
:
{},
...
...
@@ -76,35 +30,11 @@
"at"
:
3
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_trace_2_ Mf32_
27
rm_0)"
,
"target"
:
"(L_trace_2_ Mf32_
1
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_27 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_27 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"
:
3
.9
911
,
"steps"
:
1
765
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
"time"
:
2
.9
412
,
"steps"
:
1
254
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
View file @
364842fd
...
...
@@ -58,8 +58,8 @@
{
"Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
3.8529
,
"steps"
:
1
275
},
"time"
:
2.7637
,
"steps"
:
1
006
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
View file @
364842fd
[
{
"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)"
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_
5
rm_0)"
,
"pattern"
:
"L_l_RMat_of_FloatRMat$Mf32$rm"
},
"children"
:
{
"Unfold 'L_l_RMat_of_FloatRMat'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
...
...
@@ -9,7 +9,7 @@
"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_
6
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
6
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
6
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
6
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
6
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
6
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
6
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
6
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
6
[(shift_float32 a_0 8)]
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
(P_rotation_matrix
\n
{
\n
F12_RealRMat_s_a00 = Mf32_
5
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
5
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
5
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
5
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
5
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
5
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
5
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
5
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
5
[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"P_rotation_matrix{RealRMat_s}[][]"
},
"children"
:
{
"Unfold 'P_rotation_matrix'"
:
[
{
"header"
:
"Definition"
,
...
...
@@ -20,7 +20,7 @@
"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_
6
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
6
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
6
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
6
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
6
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
6
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
6
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
6
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
6
[(shift_float32 a_0 8)]
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
(L_transpose
\n
{
\n
F12_RealRMat_s_a00 = Mf32_
5
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
5
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
5
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
5
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
5
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
5
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
5
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
5
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
5
[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"L_transpose{RealRMat_s}[][][][][]"
},
"children"
:
{
"Unfold 'L_transpose'"
:
...
...
@@ -32,13 +32,13 @@
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_
6
[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_
6
[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_
6
[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_
6
[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_
6
[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_
6
[(shift_float32 a_0 5)] in
\n
let r_6 = Mf32_
6
[(shift_float32 a_0 6)] in
\n
let r_7 = Mf32_
6
[(shift_float32 a_0 7)] in
\n
let r_8 = Mf32_
6
[(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
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_
5
[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_
5
[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_
5
[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_
5
[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_
5
[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_
5
[(shift_float32 a_0 5)] in
\n
let r_6 = Mf32_
5
[(shift_float32 a_0 6)] in
\n
let r_7 = Mf32_
5
[(shift_float32 a_0 7)] in
\n
let r_8 = Mf32_
5
[(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'"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
0.3
8
},
"time"
:
0.3
2
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_11.json
View file @
364842fd
[
{
"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)"
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_
5
rm_0)"
,
"pattern"
:
"L_l_RMat_of_FloatRMat$Mf32$rm"
},
"children"
:
{
"Unfold 'L_l_RMat_of_FloatRMat'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
...
...
@@ -9,7 +9,7 @@
"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_
6
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
6
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
6
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
6
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
6
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
6
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
6
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
6
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
6
[(shift_float32 a_0 8)]
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
(P_rotation_matrix
\n
{
\n
F12_RealRMat_s_a00 = Mf32_
5
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
5
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
5
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
5
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
5
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
5
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
5
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
5
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
5
[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"P_rotation_matrix{RealRMat_s}[][]"
},
"children"
:
{
"Unfold 'P_rotation_matrix'"
:
[
{
"header"
:
"Definition"
,
...
...
@@ -32,7 +32,7 @@
"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_
6
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
6
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
6
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
6
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
6
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
6
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
6
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
6
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
6
[(shift_float32 a_0 8)]
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
(L_transpose
\n
{
\n
F12_RealRMat_s_a00 = Mf32_
5
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
5
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
5
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
5
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
5
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
5
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
5
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
5
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
5
[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"L_transpose{RealRMat_s}[][][][][]"
},
"children"
:
{
"Unfold 'L_transpose'"
:
...
...
@@ -44,7 +44,7 @@
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_
6
[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_
6
[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_
6
[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_
6
[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_
6
[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_
6
[(shift_float32 a_0 5)] in
\n
let r_6 = Mf32_
6
[(shift_float32 a_0 6)] in
\n
let r_7 = Mf32_
6
[(shift_float32 a_0 7)] in
\n
let r_8 = Mf32_
6
[(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
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_
5
[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_
5
[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_
5
[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_
5
[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_
5
[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_
5
[(shift_float32 a_0 5)] in
\n
let r_6 = Mf32_
5
[(shift_float32 a_0 6)] in
\n
let r_7 = Mf32_
5
[(shift_float32 a_0 7)] in
\n
let r_8 = Mf32_
5
[(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'"
:
...
...
@@ -56,10 +56,10 @@
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_
6
[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_
6
[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_
6
[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_
6
[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_
6
[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_
6
[(shift_float32 a_0 5)] in
\n
let r_6 = ((r_0*r_3)+(r_1*r_4)+(r_2*r_5)) in
\n
let r_7 = Mf32_
6
[(shift_float32 a_0 6)] in
\n
let r_8 = Mf32_
6
[(shift_float32 a_0 7)] in
\n
let r_9 = Mf32_
6
[(shift_float32 a_0 8)] in
\n
let r_10 = ((r_0*r_7)+(r_1*r_8)+(r_2*r_9)) in
\n
let r_11 = ((r_3*r_7)+(r_4*r_8)+(r_5*r_9)) in
\n
(EqS12_RealRMat_s
\n
{
\n
F12_RealRMat_s_a00 = (r_0*r_0)+(r_1*r_1)+(r_2*r_2) ;
\n
F12_RealRMat_s_a01 = r_6 ;
\n
F12_RealRMat_s_a02 = r_10 ;
\n
F12_RealRMat_s_a10 = r_6 ;
\n
F12_RealRMat_s_a11 = (r_3*r_3)+(r_4*r_4)+(r_5*r_5) ;
\n
F12_RealRMat_s_a12 = r_11 ;
\n
F12_RealRMat_s_a20 = r_10 ;
\n
F12_RealRMat_s_a21 = r_11 ;
\n
F12_RealRMat_s_a22 = (r_7*r_7)+(r_8*r_8)+(r_9*r_9)
\n
}
\n
{
\n
F12_RealRMat_s_a00 = 1 ;
\n
F12_RealRMat_s_a01 = 0 ;
\n
F12_RealRMat_s_a02 = 0 ;
\n
F12_RealRMat_s_a10 = 0 ;
\n
F12_RealRMat_s_a11 = 1 ;
\n
F12_RealRMat_s_a12 = 0 ;
\n
F12_RealRMat_s_a20 = 0 ;
\n
F12_RealRMat_s_a21 = 0 ;
\n
F12_RealRMat_s_a22 = 1
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_
5
[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_
5
[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_
5
[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_
5
[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_
5
[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_
5
[(shift_float32 a_0 5)] in
\n
let r_6 = ((r_0*r_3)+(r_1*r_4)+(r_2*r_5)) in
\n
let r_7 = Mf32_
5
[(shift_float32 a_0 6)] in
\n
let r_8 = Mf32_
5
[(shift_float32 a_0 7)] in
\n
let r_9 = Mf32_
5
[(shift_float32 a_0 8)] in
\n
let r_10 = ((r_0*r_7)+(r_1*r_8)+(r_2*r_9)) in
\n
let r_11 = ((r_3*r_7)+(r_4*r_8)+(r_5*r_9)) in
\n
(EqS12_RealRMat_s
\n
{
\n
F12_RealRMat_s_a00 = (r_0*r_0)+(r_1*r_1)+(r_2*r_2) ;
\n
F12_RealRMat_s_a01 = r_6 ;
\n
F12_RealRMat_s_a02 = r_10 ;
\n
F12_RealRMat_s_a10 = r_6 ;
\n
F12_RealRMat_s_a11 = (r_3*r_3)+(r_4*r_4)+(r_5*r_5) ;
\n
F12_RealRMat_s_a12 = r_11 ;
\n
F12_RealRMat_s_a20 = r_10 ;
\n
F12_RealRMat_s_a21 = r_11 ;
\n
F12_RealRMat_s_a22 = (r_7*r_7)+(r_8*r_8)+(r_9*r_9)
\n
}
\n
{
\n
F12_RealRMat_s_a00 = 1 ;
\n
F12_RealRMat_s_a01 = 0 ;
\n
F12_RealRMat_s_a02 = 0 ;
\n
F12_RealRMat_s_a10 = 0 ;
\n
F12_RealRMat_s_a11 = 1 ;
\n
F12_RealRMat_s_a12 = 0 ;
\n
F12_RealRMat_s_a20 = 0 ;
\n
F12_RealRMat_s_a21 = 0 ;
\n
F12_RealRMat_s_a22 = 1
\n
})"
,
"pattern"
:
"EqS12_RealRMat_s{RealRMat_s}{RealRMat_s}"
},
"children"
:
{
"Unfold 'EqS12_RealRMat_s'"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
5.
89
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
"time"
:
5.
56
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_12.json
deleted
100644 → 0
View file @
19613b16
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-goal"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 =
\n
(
\\
sqrt
\n
(1+Mf32_6[(shift_float32 a_0 0)]+Mf32_6[(shift_float32 a_0 4)]+
\n
Mf32_6[(shift_float32 a_0 8)])) in
\n
let m_0 = Mf32_6[(shiftfield_F7_FloatQuat_qi q_1)->1/2*r_0] in
\n
let r_1 = (2*r_0) in
\n
let m_1 =
\n
m_0[(shiftfield_F7_FloatQuat_qx q_1)
\n
->(m_0[(shift_float32 a_0 5)]-m_0[(shift_float32 a_0 7)]) div r_1] in
\n
let m_2 =
\n
m_1[(shiftfield_F7_FloatQuat_qy q_1)
\n
->(m_1[(shift_float32 a_0 6)]-m_1[(shift_float32 a_0 2)]) div r_1] in
\n
(P_unary_quaternion
\n
m_2[(shiftfield_F7_FloatQuat_qz q_1)
\n
->(m_2[(shift_float32 a_0 1)]-m_2[(shift_float32 a_0 3)]) div r_1] q_1)"
,
"pattern"
:
"P_unary_quaternion[=]$q[=]shiftfield_F7_FloatQuat_qz"
},
"children"
:
{
"Unfold 'P_unary_quaternion'"
:
[
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"valid"
,
"time"
:
1.55
,
"steps"
:
2791404
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_13.json
View file @
364842fd
...
...
@@ -10,10 +10,11 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
3.1
}
],
"Else"
:
[
{
"prover"
:
"
CVC4:1.9-prerelease:strings+counterexamples
"
,
"time"
:
3.1
9
}
],
"Else"
:
[
{
"prover"
:
"
Alt-Ergo:2.3.3
"
,
"verdict"
:
"valid"
,
"time"
:
8.12
}
]
}
}
],
"time"
:
0.8254
,
"steps"
:
724
}
]
}
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-step"
,
"at"
:
13
,
...
...
@@ -22,7 +23,7 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
3.
74
}
],
"time"
:
3.
8
}
],
"Else"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
3.
43
}
]
}
}
]
}
}
]
"time"
:
3.
56
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_14.json
View file @
364842fd
[
{
"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
\n
Mf32_1
9
[(shift_float32 a_0 4)]<Mf32_1
9
[(shift_float32 a_0 0)]"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
Mf32_1[(shift_float32 a_0 4)]<Mf32_1[(shift_float32 a_0 0)]"
,
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.0265
,
"steps"
:
28
},
"time"
:
1.8338
,
"steps"
:
10
28
},
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-step"
,
"at"
:
12
,
...
...
@@ -16,18 +16,7 @@
"Else"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
8.66
}
]
}
}
],
"Else"
:
[
{
"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"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-step"
,
"at"
:
13
,
"kind"
:
"branch"
,
...
...
@@ -35,7 +24,7 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
3.
0
2
}
],
"time"
:
3.
4
2
}
],
"Else"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
2.
78
}
]
}
}
]
}
}
]
"time"
:
2.
65
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_15.json
deleted
100644 → 0
View file @
19613b16
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_16.json
View file @
364842fd
...
...
@@ -10,11 +10,11 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
4.8
1
}
],
"time"
:
3.0
1
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
3.1779
,
"steps"
:
1003
}
]
}
}
],
"time"
:
1.0721
,
"steps"
:
734
}
]
}
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-step"
,
"at"
:
13
,
...
...
@@ -23,8 +23,8 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
4.
8
2
}
],
"time"
:
4.2
8
}
],
"Else"
:
[
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
0
.5
4
,
"steps"
:
38620
2
}
]
}
}
]
}
}
]
"time"
:
1
.5
5
,
"steps"
:
176889
2
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_17.json
View file @
364842fd
...
...
@@ -10,7 +10,7 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
6.2
}
],
"time"
:
2.83
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
...
...
@@ -22,12 +22,12 @@
"children"
:
{
"Then"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.02
98
,
"time"
:
0.02
14
,
"steps"
:
28
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
1.6341
,
"steps"
:
7
19
}
]
}
}
]
}
}
],
"time"
:
0.8667
,
"steps"
:
7
24
}
]
}
}
]
}
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
4.245
5
,
"steps"
:
1
533
}
]
}
}
]
"time"
:
1.41
5
,
"steps"
:
1
015
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_18.json
View file @
364842fd
...
...
@@ -10,7 +10,7 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
5.
7
}
],
"time"
:
2.8
7
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
...
...
@@ -22,12 +22,12 @@
"children"
:
{
"Then"
:
[
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"valid"
,
"time"
:
0.0
8
,
"steps"
:
1
86302
}
],
"time"
:
0.0
9
,
"steps"
:
1
90040
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
1.6261
,
"steps"
:
72
1
}
]
}
}
]
}
}
],
"time"
:
0.9535
,
"steps"
:
72
6
}
]
}
}
]
}
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
5.1
29
8
,
"steps"
:
1
537
}
]
}
}
]
"time"
:
1.27
29
,
"steps"
:
1
019
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_19.json
View file @
364842fd
...
...
@@ -10,7 +10,7 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
2.52
}
],
"time"
:
3.45
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
...
...
@@ -22,12 +22,12 @@
"children"
:
{
"Then"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.0
304
,
"time"
:
0.0
226
,
"steps"
:
28
}
],
"Else"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
5.1
}
]
}
}
]
}
}
],
"time"
:
1.97
}
]
}
}
]
}
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-step"
,
"at"
:
13
,
...
...
@@ -36,8 +36,8 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
4.2
4
}
],
"time"
:
5.8
4
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
1.
6757
,
"steps"
:
72
3
}
]
}
}
]
}
}
]
"time"
:
1.
113
,
"steps"
:
72
5
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_2.json
View file @
364842fd
[
{
"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)"
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_
5
rm_0)"
,
"pattern"
:
"L_l_RMat_of_FloatRMat$Mf32$rm"
},
"children"
:
{
"Unfold 'L_l_RMat_of_FloatRMat'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
...
...
@@ -9,7 +9,7 @@
"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_
6
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
6
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
6
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
6
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
6
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
6
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
6
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
6
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
6
[(shift_float32 a_0 8)]
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
(P_rotation_matrix
\n
{
\n
F12_RealRMat_s_a00 = Mf32_
5
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
5
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
5
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
5
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
5
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
5
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
5
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
5
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
5
[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"P_rotation_matrix{RealRMat_s}[][]"
},
"children"
:
{
"Unfold 'P_rotation_matrix'"
:
[
{
"header"
:
"Definition"
,
...
...
@@ -20,7 +20,7 @@
"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_
6
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
6
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
6
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
6
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
6
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
6
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
6
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
6
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
6
[(shift_float32 a_0 8)]
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
(L_transpose
\n
{
\n
F12_RealRMat_s_a00 = Mf32_
5
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
5
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
5
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
5
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
5
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
5
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
5
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
5
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
5
[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"L_transpose{RealRMat_s}[][][][][]"
},
"children"
:
{
"Unfold 'L_transpose'"
:
...
...
@@ -44,14 +44,14 @@
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_
6
[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_
6
[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_
6
[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_
6
[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_
6
[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_
6
[(shift_float32 a_0 5)] in
\n
let r_6 = Mf32_
6
[(shift_float32 a_0 6)] in
\n
let r_7 = Mf32_
6
[(shift_float32 a_0 7)] in
\n
let r_8 = Mf32_
6
[(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
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_
5
[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_
5
[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_
5
[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_
5
[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_
5
[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_
5
[(shift_float32 a_0 5)] in
\n
let r_6 = Mf32_
5
[(shift_float32 a_0 6)] in
\n
let r_7 = Mf32_
5
[(shift_float32 a_0 7)] in
\n
let r_8 = Mf32_
5
[(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'"
:
[
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
0.
55
,
"steps"
:
5
38468
},
"time"
:
0.
49
,
"steps"
:
5
48633
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_20.json
View file @
364842fd
...
...
@@ -10,7 +10,7 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
3.56
}
],
"time"
:
2.34
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
...
...
@@ -22,12 +22,12 @@
"children"
:
{
"Then"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.04
1
4
,
"time"
:
0.044
8
,
"steps"
:
28
}
],
"Else"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,