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
d503e723
Commit
d503e723
authored
Apr 30, 2021
by
POLLIEN Baptiste
Browse files
Merge and update of wp script
parents
503e4737
857e39ff
Changes
40
Hide whitespace changes
Inline
Side-by-side
Showing
20 changed files
with
194 additions
and
229 deletions
+194
-229
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
+1
-1
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
+1
-1
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
+1
-1
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
...irborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
+122
-9
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
-81
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
+9
-31
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
+2
-2
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_21.json
...orne/.frama-c/wp/script/float_quat_of_rmat_assert_21.json
+2
-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
+1
-1
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
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_312_ensures_2.json
...frama-c/wp/script/float_rmat_of_eulers_312_ensures_2.json
+4
-31
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_321_ensures.json
.../.frama-c/wp/script/float_rmat_of_eulers_321_ensures.json
+8
-8
No files found.
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
View file @
d503e723
...
...
@@ -89,5 +89,5 @@
{
"Unfold 'L_l_RMat_of_FloatRMat'"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
1.
5505
,
"time"
:
1.
404
,
"steps"
:
989
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
View file @
d503e723
...
...
@@ -36,5 +36,5 @@
{
"Unfold 'L_trace_2_'"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
2.
7065
,
"time"
:
2.
5856
,
"steps"
:
1249
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
View file @
d503e723
...
...
@@ -58,7 +58,7 @@
{
"Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
2.4316
,
"time"
:
1.8028
,
"steps"
:
1008
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
View file @
d503e723
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-step"
,
"at"
:
8
,
"kind"
:
"branch"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
0<
\n
(Mf32_1[(shift_float32 a_0 0)]+Mf32_1[(shift_float32 a_0 4)]+
\n
Mf32_1[(shift_float32 a_0 8)])"
,
"pattern"
:
"<0+[][][]$Mf32shift_float32$Mf32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
0.31
,
"steps"
:
404607
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
3.7782
,
"steps"
:
1331
}
]
}
}
]
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_1 rm_0)"
,
"pattern"
:
"L_l_RMat_of_FloatRMat$Mf32$rm"
},
"children"
:
{
"Unfold 'L_l_RMat_of_FloatRMat'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
(P_rotation_matrix
\n
{
\n
F12_RealRMat_s_a00 = Mf32_1[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_1[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_1[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_1[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_1[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_1[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_1[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_1[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_1[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"P_rotation_matrix{RealRMat_s}[][]"
},
"children"
:
{
"Unfold 'P_rotation_matrix'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
(L_transpose
\n
{
\n
F12_RealRMat_s_a00 = Mf32_1[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_1[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_1[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_1[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_1[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_1[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_1[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_1[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_1[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"L_transpose{RealRMat_s}[][][][][]"
},
"children"
:
{
"Unfold 'L_transpose'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_1[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_1[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_1[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_1[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_1[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_1[(shift_float32 a_0 5)] in
\n
let r_6 = Mf32_1[(shift_float32 a_0 6)] in
\n
let r_7 = Mf32_1[(shift_float32 a_0 7)] in
\n
let r_8 = Mf32_1[(shift_float32 a_0 8)] in
\n
(L_mult_RealRMat
\n
{
\n
F12_RealRMat_s_a00 = r_0 ;
\n
F12_RealRMat_s_a01 = r_1 ;
\n
F12_RealRMat_s_a02 = r_2 ;
\n
F12_RealRMat_s_a10 = r_3 ;
\n
F12_RealRMat_s_a11 = r_4 ;
\n
F12_RealRMat_s_a12 = r_5 ;
\n
F12_RealRMat_s_a20 = r_6 ;
\n
F12_RealRMat_s_a21 = r_7 ;
\n
F12_RealRMat_s_a22 = r_8
\n
}
\n
{
\n
F12_RealRMat_s_a00 = r_0 ;
\n
F12_RealRMat_s_a01 = r_3 ;
\n
F12_RealRMat_s_a02 = r_6 ;
\n
F12_RealRMat_s_a10 = r_1 ;
\n
F12_RealRMat_s_a11 = r_4 ;
\n
F12_RealRMat_s_a12 = r_7 ;
\n
F12_RealRMat_s_a20 = r_2 ;
\n
F12_RealRMat_s_a21 = r_5 ;
\n
F12_RealRMat_s_a22 = r_8
\n
})"
,
"pattern"
:
"L_mult_RealRMat{RealRMat_s}{RealRMat_s}"
},
"children"
:
{
"Unfold 'L_mult_RealRMat'"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-step"
,
"at"
:
8
,
"kind"
:
"branch"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
0<
\n
(Mf32_1[(shift_float32 a_0 0)]+Mf32_1[(shift_float32 a_0 4)]+
\n
Mf32_1[(shift_float32 a_0 8)])"
,
"pattern"
:
"<0+[][][]$Mf32shift_float32$Mf32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
0.29
,
"steps"
:
426627
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-step"
,
"at"
:
10
,
"kind"
:
"branch"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\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"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
0.33
,
"steps"
:
389571
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-step"
,
"at"
:
16
,
"kind"
:
"branch"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
Mf32_1[(shift_float32 a_0 8)]<Mf32_1[(shift_float32 a_0 4)]"
,
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"valid"
,
"time"
:
0.04
,
"steps"
:
202708
}
],
"Else"
:
[
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
0.35
,
"steps"
:
387857
}
]
}
}
]
}
}
],
"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"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
0.29
,
"steps"
:
382945
}
],
"Else"
:
[
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
0.51
,
"steps"
:
385200
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_11.json
View file @
d503e723
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_
7
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_
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
})"
,
"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_
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
})"
,
"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_
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
})"
,
"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_
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
})"
,
"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.56
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
"time"
:
4
.
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_12.json
deleted
100644 → 0
View file @
503e4737
[
{
"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_14.json
View file @
d503e723
[
{
"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.0185
,
"steps"
:
28
},
"time"
:
1.8157
,
"steps"
:
1043
},
{
"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"
:
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"
,
"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.4
2
}
],
"time"
:
2.8
2
}
],
"Else"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
2.
6
5
}
]
}
}
]
}
}
]
"time"
:
2.5
8
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_15.json
deleted
100644 → 0
View file @
503e4737
[
{
"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 @
d503e723
[
{
"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_
27
[(shift_float32 a_0 4)]<Mf32_
27
[(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"
:
"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"
,
"children"
:
{
"Then"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-step"
,
"at"
:
12
,
"kind"
:
"branch"
,
...
...
@@ -21,23 +10,12 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
4.71
}
],
"time"
:
3.3
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"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"
,
"time"
:
1.0284
,
"steps"
:
744
}
]
}
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-step"
,
"at"
:
13
,
"kind"
:
"branch"
,
...
...
@@ -45,8 +23,8 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
5.05
}
],
"time"
:
2.72
}
],
"Else"
:
[
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
0.65
,
"steps"
:
388735
}
]
}
}
]
}
}
]
"time"
:
1.56
,
"steps"
:
1772689
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_17.json
View file @
d503e723
...
...
@@ -10,7 +10,7 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
4.71
}
],
"time"
:
2.89
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
...
...
@@ -22,12 +22,12 @@
"children"
:
{
"Then"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.0
389
,
"time"
:
0.0
216
,
"steps"
:
28
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
2.421
,
"steps"
:
7
21
}
]
}
}
]
}
}
],
"time"
:
0.9114
,
"steps"
:
7
34
}
]
}
}
]
}
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
5.71
76
,
"steps"
:
1
54
0
}
]
}
}
]
"time"
:
1.56
76
,
"steps"
:
1
03
0
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_18.json
View file @
d503e723
...
...
@@ -10,7 +10,7 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
6.0
6
}
],
"time"
:
2.7
6
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
...
...
@@ -22,12 +22,12 @@
"children"
:
{
"Then"
:
[
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"valid"
,
"time"
:
0.
1
,
"steps"
:
187519
}
],
"time"
:
0.
04
,
"steps"
:
214932
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
1.
9234
,
"steps"
:
7
25
}
]
}
}
]
}
}
],
"time"
:
1.
0655
,
"steps"
:
7
36
}
]
}
}
]
}
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
4.923
1
,
"steps"
:
1
542
}
]
}
}
]
"time"
:
1.641
1
,
"steps"
:
1
034
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_19.json
View file @
d503e723
...
...
@@ -10,7 +10,7 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
5.86
}
],
"time"
:
3.42
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
...
...
@@ -22,12 +22,12 @@
"children"
:
{
"Then"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.0
65
4
,
"time"
:
0.04
9
,
"steps"
:
28
}
],
"Else"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
3.23
}
]
}
}
]
}
}
],
"time"
:
1.95
}
]
}
}
]
}
}
],
"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.39
}
],
"time"
:
3.95
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
2.358
,
"steps"
:
7
2
5
}
]
}
}
]
}
}
]
"time"
:
0.981
,
"steps"
:
7
3
5
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_2.json
View file @
d503e723
...
...
@@ -3,6 +3,6 @@
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
0<
\n
(Mf32_1[(shift_float32 a_0 0)]+Mf32_1[(shift_float32 a_0 4)]+
\n
Mf32_1[(shift_float32 a_0 8)])"
,
"pattern"
:
"<0+[][][]$Mf32shift_float32$Mf32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.
7925
,
"steps"
:
722
}
],
"time"
:
0.
8391
,
"steps"
:
722
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
4.
5395
,
"steps"
:
1331
}
]
}
}
]
"time"
:
4.
943
,
"steps"
:
1331
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_20.json
View file @
d503e723
...
...
@@ -10,7 +10,7 @@
"pattern"
:
"<[][]$Mf32shift_float32$Mf32shift_float32"
},
"children"
:
{
"Then"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
2.
33
}
],
"time"
:
2.
89
}
],
"Else"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
...
...
@@ -22,12 +22,12 @@
"children"
:
{
"Then"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.0
506
,
"time"
:
0.0
488
,
"steps"
:
28
}
],
"Else"
: