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
7ffcf1a3
Commit
7ffcf1a3
authored
Apr 26, 2021
by
POLLIEN Baptiste
Browse files
Fix smoke tests
parent
364842fd
Changes
24
Hide whitespace changes
Inline
Side-by-side
Showing
20 changed files
with
209 additions
and
82 deletions
+209
-82
sw/airborne/.frama-c/wp/script/fabsf_wp_smoke_dead_call_s1100.json
...ne/.frama-c/wp/script/fabsf_wp_smoke_dead_call_s1100.json
+7
-0
sw/airborne/.frama-c/wp/script/float_mat2_mult_wp_smoke_default_requires.json
.../wp/script/float_mat2_mult_wp_smoke_default_requires.json
+7
-0
sw/airborne/.frama-c/wp/script/float_mat_inv_2d_wp_smoke_dead_code_s1102.json
.../wp/script/float_mat_inv_2d_wp_smoke_dead_code_s1102.json
+7
-0
sw/airborne/.frama-c/wp/script/float_mat_inv_2d_wp_smoke_dead_code_s1104.json
.../wp/script/float_mat_inv_2d_wp_smoke_dead_code_s1104.json
+7
-0
sw/airborne/.frama-c/wp/script/float_mat_inv_2d_wp_smoke_default_requires.json
...wp/script/float_mat_inv_2d_wp_smoke_default_requires.json
+7
-0
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
+2
-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
+2
-2
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
+4
-4
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
+5
-5
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
+81
-0
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
+0
-29
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
+14
-3
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
+7
-0
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
+31
-9
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
+5
-5
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
+4
-4
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
No files found.
sw/airborne/.frama-c/wp/script/fabsf_wp_smoke_dead_call_s1100.json
0 → 100644
View file @
7ffcf1a3
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
}
]
sw/airborne/.frama-c/wp/script/float_mat2_mult_wp_smoke_default_requires.json
0 → 100644
View file @
7ffcf1a3
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
}
]
sw/airborne/.frama-c/wp/script/float_mat_inv_2d_wp_smoke_dead_code_s1102.json
0 → 100644
View file @
7ffcf1a3
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
}
]
sw/airborne/.frama-c/wp/script/float_mat_inv_2d_wp_smoke_dead_code_s1104.json
0 → 100644
View file @
7ffcf1a3
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
}
]
sw/airborne/.frama-c/wp/script/float_mat_inv_2d_wp_smoke_default_requires.json
0 → 100644
View file @
7ffcf1a3
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
2
.
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
View file @
7ffcf1a3
...
...
@@ -89,5 +89,5 @@
{
"Unfold 'L_l_RMat_of_FloatRMat'"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
1.
148
,
"steps"
:
9
74
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
"time"
:
1.
2306
,
"steps"
:
9
91
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
View file @
7ffcf1a3
...
...
@@ -36,5 +36,5 @@
{
"Unfold 'L_trace_2_'"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
2.9412
,
"steps"
:
12
54
}
]
}
}
]
}
}
]
}
}
]
}
}
]
"time"
:
10.1966
,
"steps"
:
12
88
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
View file @
7ffcf1a3
...
...
@@ -58,8 +58,8 @@
{
"Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
2.7637
,
"steps"
:
1
006
},
"time"
:
10.5394
,
"steps"
:
1
289
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
View file @
7ffcf1a3
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_
5
rm_0)"
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_
7
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_
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
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
(P_rotation_matrix
\n
{
\n
F12_RealRMat_s_a00 = Mf32_
7
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
7
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
7
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
7
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
7
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
7
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
7
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
7
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
7
[(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_
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
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
(L_transpose
\n
{
\n
F12_RealRMat_s_a00 = Mf32_
7
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
7
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
7
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
7
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
7
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
7
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
7
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
7
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
7
[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"L_transpose{RealRMat_s}[][][][][]"
},
"children"
:
{
"Unfold 'L_transpose'"
:
...
...
@@ -32,7 +32,7 @@
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"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
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_
7
[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_
7
[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_
7
[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_
7
[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_
7
[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_
7
[(shift_float32 a_0 5)] in
\n
let r_6 = Mf32_
7
[(shift_float32 a_0 6)] in
\n
let r_7 = Mf32_
7
[(shift_float32 a_0 7)] in
\n
let r_8 = Mf32_
7
[(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'"
:
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_11.json
View file @
7ffcf1a3
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_
5
rm_0)"
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_
7
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_
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
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
(P_rotation_matrix
\n
{
\n
F12_RealRMat_s_a00 = Mf32_
7
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
7
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
7
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
7
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
7
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
7
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
7
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
7
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
7
[(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_
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
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
(L_transpose
\n
{
\n
F12_RealRMat_s_a00 = Mf32_
7
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
7
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
7
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
7
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
7
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
7
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
7
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
7
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
7
[(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_
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
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_
7
[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_
7
[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_
7
[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_
7
[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_
7
[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_
7
[(shift_float32 a_0 5)] in
\n
let r_6 = Mf32_
7
[(shift_float32 a_0 6)] in
\n
let r_7 = Mf32_
7
[(shift_float32 a_0 7)] in
\n
let r_8 = Mf32_
7
[(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,7 +56,7 @@
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"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
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_
7
[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_
7
[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_
7
[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_
7
[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_
7
[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_
7
[(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_
7
[(shift_float32 a_0 6)] in
\n
let r_8 = Mf32_
7
[(shift_float32 a_0 7)] in
\n
let r_9 = Mf32_
7
[(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'"
:
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_12.json
0 → 100644
View file @
7ffcf1a3
[
{
"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
.
},
{
"prover"
:
"script"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 =
\n
(
\\
sqrt
\n
(1+Mf32_7[(shift_float32 a_0 0)]+Mf32_7[(shift_float32 a_0 4)]+
\n
Mf32_7[(shift_float32 a_0 8)])) in
\n
let m_0 = Mf32_7[(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
(L_l_RMat_of_FloatQuat
\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"
:
"L_l_RMat_of_FloatQuat[=]$q[=]shiftfield_F7_FloatQuat_qz"
},
"children"
:
{
"Unfold 'L_l_RMat_of_FloatQuat'"
:
[
{
"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
.
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 =
\n
(
\\
sqrt
\n
(1+Mf32_7[(shift_float32 a_0 0)]+Mf32_7[(shift_float32 a_0 4)]+
\n
Mf32_7[(shift_float32 a_0 8)])) in
\n
let m_0 = Mf32_7[(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
(L_l_RMat_of_FloatRMat
\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] rm_0)"
,
"pattern"
:
"L_l_RMat_of_FloatRMat[=]$rm[=]shiftfield_F7_FloatQuat_qz"
},
"children"
:
{
"Unfold 'L_l_RMat_of_FloatRMat'"
:
[
{
"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
.
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_7[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_7[(shift_float32 a_0 4)] in
\n
let r_2 = Mf32_7[(shift_float32 a_0 8)] in
\n
let r_3 = (
\\
sqrt (1+r_0+r_1+r_2)) in
\n
let m_0 = Mf32_7[(shiftfield_F7_FloatQuat_qi q_1)->1/2*r_3] in
\n
let a_1 = (shift_float32 a_0 7) in
\n
let a_2 = (shift_float32 a_0 5) in
\n
let r_4 = (2*r_3) in
\n
let m_1 =
\n
m_0[(shiftfield_F7_FloatQuat_qx q_1)->(m_0[a_2]-m_0[a_1]) div r_4] in
\n
let a_3 = (shift_float32 a_0 2) in
\n
let a_4 = (shift_float32 a_0 6) in
\n
let m_2 =
\n
m_1[(shiftfield_F7_FloatQuat_qy q_1)->(m_1[a_4]-m_1[a_3]) div r_4] in
\n
let a_5 = (shift_float32 a_0 3) in
\n
let a_6 = (shift_float32 a_0 1) in
\n
let m_3 =
\n
m_2[(shiftfield_F7_FloatQuat_qz q_1)->(m_2[a_6]-m_2[a_5]) div r_4] in
\n
(L_transpose
\n
{
\n
F12_RealRMat_s_a00 = r_0 ;
\n
F12_RealRMat_s_a01 = m_3[a_6] ;
\n
F12_RealRMat_s_a02 = m_3[a_3] ;
\n
F12_RealRMat_s_a10 = m_3[a_5] ;
\n
F12_RealRMat_s_a11 = r_1 ;
\n
F12_RealRMat_s_a12 = m_3[a_2] ;
\n
F12_RealRMat_s_a20 = m_3[a_4] ;
\n
F12_RealRMat_s_a21 = m_3[a_1] ;
\n
F12_RealRMat_s_a22 = r_2
\n
})"
,
"pattern"
:
"L_transpose{RealRMat_s}[][][][][]"
},
"children"
:
{
"Unfold 'L_transpose'"
:
[
{
"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_13.json
deleted
100644 → 0
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[(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
\n
Mf32_1[(shift_float32 a_0 8)]<Mf32_1[(shift_float32 a_0 0)]"
,
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
3.19
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.8254
,
"steps"
:
724
}
]
}
}
],
"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
\n
Mf32_1[(shift_float32 a_0 8)]<Mf32_1[(shift_float32 a_0 4)]"
,
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
3.8
}
],
"Else"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
3.56
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_14.json
View file @
7ffcf1a3
[
{
"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[(shift_float32 a_0 4)]<Mf32_1[(shift_float32 a_0 0)]"
,
"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)]"
,
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
1.8338
,
"steps"
:
10
28
},
"time"
:
0.0185
,
"steps"
:
28
},
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-step"
,
"at"
:
12
,
...
...
@@ -16,7 +16,18 @@
"Else"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
8.66
}
]
}
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"Else"
:
[
{
"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
.
},
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-step"
,
"at"
:
13
,
"kind"
:
"branch"
,
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_15.json
0 → 100644
View file @
7ffcf1a3
[
{
"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 @
7ffcf1a3
[
{
"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
[(shift_float32 a_0 4)]<Mf32_
1
[(shift_float32 a_0 0)]"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
Mf32_
27
[(shift_float32 a_0 4)]<Mf32_
27
[(shift_float32 a_0 0)]"
,
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"children"
:
{
"Then"
:
[
{
"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
.
},
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-step"
,
"at"
:
12
,
"kind"
:
"branch"
,
...
...
@@ -10,12 +21,23 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
3.0
1
}
],
"time"
:
4.7
1
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
1.0721
,
"steps"
:
734
}
]
}
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"time"
:
2.6697
,
"steps"
:
1010
}
]
}
}
],
"Else"
:
[
{
"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
.
},
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-step"
,
"at"
:
13
,
"kind"
:
"branch"
,
...
...
@@ -23,8 +45,8 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
4.28
}
],
"time"
:
5.05
}
],
"Else"
:
[
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
1.5
5
,
"steps"
:
1768892
}
]
}
}
]
}
}
]
"time"
:
0.6
5
,
"steps"
:
388735
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_17.json
View file @
7ffcf1a3
...
...
@@ -10,7 +10,7 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
2.83
}
],
"time"
:
4.71
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
...
...
@@ -22,12 +22,12 @@
"children"
:
{
"Then"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.0
214
,
"time"
:
0.0
389
,
"steps"
:
28
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.8667
,
"steps"
:
72
4
}
]
}
}
]
}
}
],
"time"
:
2.421
,
"steps"
:
72
1
}
]
}
}
]
}
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
1.415
,
"steps"
:
1
015
}
]
}
}
]
"time"
:
5.7176
,
"steps"
:
1
540
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_18.json
View file @
7ffcf1a3
...
...
@@ -10,7 +10,7 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
2.87
}
],
"time"
:
6.06
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
...
...
@@ -22,12 +22,12 @@
"children"
:
{
"Then"
:
[
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"valid"
,
"time"
:
0.
09
,
"steps"
:
1
90040
}
],
"time"
:
0.
1
,
"steps"
:
1
87519
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0
.9
535
,
"steps"
:
72
6
}
]
}
}
]
}
}
],
"time"
:
1
.9
234
,
"steps"
:
72
5
}
]
}
}
]
}
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
1.2729
,
"steps"
:
1
019
}
]
}
}
]
"time"
:
4.9231
,
"steps"
:
1
542
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_19.json
View file @
7ffcf1a3
...
...
@@ -10,7 +10,7 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
3.45
}
],
"time"
:
5.86
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
...
...
@@ -22,12 +22,12 @@
"children"
:
{
"Then"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.0
226
,
"time"
:
0.0
654
,
"steps"
:
28
}
],
"Else"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
1.97
}
]
}
}
]
}
}
],
"time"
:
3.23
}
]
}
}
]
}
}
],
"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"
:
5.84
}
],
"time"
:
4.39
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
1.113
,
"time"
:
2.358
,
"steps"
:
725
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_2.json
View file @
7ffcf1a3
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_
5
rm_0)"
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_
7
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_
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
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
(P_rotation_matrix
\n
{
\n
F12_RealRMat_s_a00 = Mf32_
7
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
7
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
7
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
7
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
7
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
7
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
7
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
7
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
7
[(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_
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
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
(L_transpose
\n
{
\n
F12_RealRMat_s_a00 = Mf32_
7
[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_
7
[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_
7
[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_
7
[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_
7
[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_
7
[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_
7
[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_
7
[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_
7
[(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_
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
})"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_
7
[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_
7
[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_
7
[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_
7
[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_
7
[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_
7
[(shift_float32 a_0 5)] in
\n
let r_6 = Mf32_
7
[(shift_float32 a_0 6)] in
\n
let r_7 = Mf32_
7
[(shift_float32 a_0 7)] in
\n
let r_8 = Mf32_
7
[(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'"
:
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_20.json
View file @
7ffcf1a3
...
...
@@ -10,7 +10,7 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
2.3
4
}
],
"time"
:
2.3
3
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
...
...
@@ -22,12 +22,12 @@
"children"
:
{
"Then"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.0
448
,
"time"
:
0.0
506
,