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
7ba71702
Commit
7ba71702
authored
Apr 27, 2021
by
POLLIEN Baptiste
Browse files
Merge branch 'functional-verification'
parents
32eb4a61
96c450c0
Changes
49
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
20 changed files
with
1737 additions
and
103 deletions
+1737
-103
README.md
README.md
+7
-0
sw/airborne/.frama-c/wp/interactive/lemma_float_rmat_of_eulers_321_1.v
...frama-c/wp/interactive/lemma_float_rmat_of_eulers_321_1.v
+644
-0
sw/airborne/.frama-c/wp/interactive/lemma_float_rmat_of_eulers_321_2.v
...frama-c/wp/interactive/lemma_float_rmat_of_eulers_321_2.v
+667
-0
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
+16
-16
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
+4
-57
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
+8
-4
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
...irborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
+12
-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
+65
-0
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
+70
-17
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
+41
-0
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
+52
-0
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
+33
-0
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
+33
-0
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
+43
-0
No files found.
README.md
View file @
7ba71702
...
...
@@ -40,6 +40,13 @@ launch the script that start the analysis:
./frama-c-analysis.sh
```
The WP smoke tests can be enable with the environment variable
`SMOKE`
as follow:
```
SMOKE=1 ./frama-c-analysis.sh
```
Quick descritpion of modified files:
------------------------------------
...
...
sw/airborne/.frama-c/wp/interactive/lemma_float_rmat_of_eulers_321_1.v
0 → 100644
View file @
7ba71702
This diff is collapsed.
Click to expand it.
sw/airborne/.frama-c/wp/interactive/lemma_float_rmat_of_eulers_321_2.v
0 → 100644
View file @
7ba71702
This diff is collapsed.
Click to expand it.
sw/airborne/.frama-c/wp/script/fabsf_wp_smoke_dead_call_s1100.json
0 → 100644
View file @
7ba71702
[
{
"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 @
7ba71702
[
{
"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 @
7ba71702
[
{
"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 @
7ba71702
[
{
"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 @
7ba71702
[
{
"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 @
7ba71702
...
...
@@ -18,7 +18,7 @@
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F
6
_FloatRMat_m rm_0) in
\n
(L_transpose
\n
{
\n
F
9
_RealRMat_s_a00 = Mf32_0[(shift_float32 a_0 0)] ;
\n
F
9
_RealRMat_s_a01 = Mf32_0[(shift_float32 a_0 1)] ;
\n
F
9
_RealRMat_s_a02 = Mf32_0[(shift_float32 a_0 2)] ;
\n
F
9
_RealRMat_s_a10 = Mf32_0[(shift_float32 a_0 3)] ;
\n
F
9
_RealRMat_s_a11 = Mf32_0[(shift_float32 a_0 4)] ;
\n
F
9
_RealRMat_s_a12 = Mf32_0[(shift_float32 a_0 5)] ;
\n
F
9
_RealRMat_s_a20 = Mf32_0[(shift_float32 a_0 6)] ;
\n
F
9
_RealRMat_s_a21 = Mf32_0[(shift_float32 a_0 7)] ;
\n
F
9
_RealRMat_s_a22 = Mf32_0[(shift_float32 a_0 8)]
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F
9
_FloatRMat_m rm_0) in
\n
(L_transpose
\n
{
\n
F
12
_RealRMat_s_a00 = Mf32_0[(shift_float32 a_0 0)] ;
\n
F
12
_RealRMat_s_a01 = Mf32_0[(shift_float32 a_0 1)] ;
\n
F
12
_RealRMat_s_a02 = Mf32_0[(shift_float32 a_0 2)] ;
\n
F
12
_RealRMat_s_a10 = Mf32_0[(shift_float32 a_0 3)] ;
\n
F
12
_RealRMat_s_a11 = Mf32_0[(shift_float32 a_0 4)] ;
\n
F
12
_RealRMat_s_a12 = Mf32_0[(shift_float32 a_0 5)] ;
\n
F
12
_RealRMat_s_a20 = Mf32_0[(shift_float32 a_0 6)] ;
\n
F
12
_RealRMat_s_a21 = Mf32_0[(shift_float32 a_0 7)] ;
\n
F
12
_RealRMat_s_a22 = Mf32_0[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"L_transpose{RealRMat_s}[][][][][]"
},
"children"
:
{
"Unfold 'L_transpose'"
:
...
...
@@ -28,7 +28,7 @@
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F
6
_FloatRMat_m rm_0) in
\n
(L_l_FloatQuat_of_RMat_0_max_1_
\n
{
\n
F
9
_RealRMat_s_a00 = Mf32_0[(shift_float32 a_0 0)] ;
\n
F
9
_RealRMat_s_a01 = Mf32_0[(shift_float32 a_0 3)] ;
\n
F
9
_RealRMat_s_a02 = Mf32_0[(shift_float32 a_0 6)] ;
\n
F
9
_RealRMat_s_a10 = Mf32_0[(shift_float32 a_0 1)] ;
\n
F
9
_RealRMat_s_a11 = Mf32_0[(shift_float32 a_0 4)] ;
\n
F
9
_RealRMat_s_a12 = Mf32_0[(shift_float32 a_0 7)] ;
\n
F
9
_RealRMat_s_a20 = Mf32_0[(shift_float32 a_0 2)] ;
\n
F
9
_RealRMat_s_a21 = Mf32_0[(shift_float32 a_0 5)] ;
\n
F
9
_RealRMat_s_a22 = Mf32_0[(shift_float32 a_0 8)]
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F
9
_FloatRMat_m rm_0) in
\n
(L_l_FloatQuat_of_RMat_0_max_1_
\n
{
\n
F
12
_RealRMat_s_a00 = Mf32_0[(shift_float32 a_0 0)] ;
\n
F
12
_RealRMat_s_a01 = Mf32_0[(shift_float32 a_0 3)] ;
\n
F
12
_RealRMat_s_a02 = Mf32_0[(shift_float32 a_0 6)] ;
\n
F
12
_RealRMat_s_a10 = Mf32_0[(shift_float32 a_0 1)] ;
\n
F
12
_RealRMat_s_a11 = Mf32_0[(shift_float32 a_0 4)] ;
\n
F
12
_RealRMat_s_a12 = Mf32_0[(shift_float32 a_0 7)] ;
\n
F
12
_RealRMat_s_a20 = Mf32_0[(shift_float32 a_0 2)] ;
\n
F
12
_RealRMat_s_a21 = Mf32_0[(shift_float32 a_0 5)] ;
\n
F
12
_RealRMat_s_a22 = Mf32_0[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"L_l_FloatQuat_of_RMat_0_max_1_{RealRMat_s}"
},
"children"
:
{
"Unfold 'L_l_FloatQuat_of_RMat_0_max_1_'"
:
...
...
@@ -36,15 +36,6 @@
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-goal"
,
"target"
:
"let a_0 = (shiftfield_F6_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
(EqS10_RealQuat_s
\n
{
\n
F10_RealQuat_s_qi =
\n
(Mf32_0[(shift_float32 a_0 5)]-Mf32_0[(shift_float32 a_0 7)]) div r_1 ;
\n
F10_RealQuat_s_qx = 1/2*r_0 ;
\n
F10_RealQuat_s_qy =
\n
(Mf32_0[(shift_float32 a_0 1)]+Mf32_0[(shift_float32 a_0 3)]) div r_1 ;
\n
F10_RealQuat_s_qz =
\n
(Mf32_0[(shift_float32 a_0 2)]+Mf32_0[(shift_float32 a_0 6)]) 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_Quat_of_FloatQuat Mf32_0 q_0)"
,
...
...
@@ -55,11 +46,20 @@
"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_
27
rm_0)"
,
"target"
:
"(L_trace_2_ Mf32_
1
rm_0)"
,
"pattern"
:
"L_trace_2_$Mf32$rm"
},
"children"
:
{
"Unfold 'L_trace_2_'"
:
...
...
@@ -71,7 +71,7 @@
"at"
:
3
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_
27
rm_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_'"
:
...
...
@@ -83,11 +83,11 @@
"at"
:
3
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_
27
rm_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"
:
4.9965
,
"steps"
:
1942
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
"time"
:
1.2306
,
"steps"
:
991
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
View file @
7ba71702
...
...
@@ -18,7 +18,7 @@
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"let a_0 = (L_l_RMat_of_FloatRMat Mf32_0 rm_0) in
\n
(L_l_FloatQuat_of_RMat_1_max_1_
\n
{
\n
a_0 with
\n
F
9
_RealRMat_s_a01 = a_0.F
9
_RealRMat_s_a10 ;
\n
F
9
_RealRMat_s_a02 = a_0.F
9
_RealRMat_s_a20 ;
\n
F
9
_RealRMat_s_a10 = a_0.F
9
_RealRMat_s_a01 ;
\n
F
9
_RealRMat_s_a12 = a_0.F
9
_RealRMat_s_a21 ;
\n
F
9
_RealRMat_s_a20 = a_0.F
9
_RealRMat_s_a02 ;
\n
F
9
_RealRMat_s_a21 = a_0.F
9
_RealRMat_s_a12
\n
})"
,
"target"
:
"let a_0 = (L_l_RMat_of_FloatRMat Mf32_0 rm_0) in
\n
(L_l_FloatQuat_of_RMat_1_max_1_
\n
{
\n
a_0 with
\n
F
12
_RealRMat_s_a01 = a_0.F
12
_RealRMat_s_a10 ;
\n
F
12
_RealRMat_s_a02 = a_0.F
12
_RealRMat_s_a20 ;
\n
F
12
_RealRMat_s_a10 = a_0.F
12
_RealRMat_s_a01 ;
\n
F
12
_RealRMat_s_a12 = a_0.F
12
_RealRMat_s_a21 ;
\n
F
12
_RealRMat_s_a20 = a_0.F
12
_RealRMat_s_a02 ;
\n
F
12
_RealRMat_s_a21 = a_0.F
12
_RealRMat_s_a12
\n
})"
,
"pattern"
:
"L_l_FloatQuat_of_RMat_1_max_1_{RealRMat_s}"
},
"children"
:
{
"Unfold 'L_l_FloatQuat_of_RMat_1_max_1_'"
:
...
...
@@ -26,68 +26,15 @@
"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"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"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.9911
,
"steps"
:
1
765
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
"time"
:
10.1966
,
"steps"
:
1
288
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
View file @
7ba71702
...
...
@@ -20,7 +20,7 @@
"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_'"
:
...
...
@@ -32,7 +32,7 @@
"at"
:
3
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_
27
rm_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_'"
:
...
...
@@ -52,11 +52,15 @@
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"let a_0 = (L_l_RMat_of_FloatRMat Mf32_0 rm_0) in
\n
(L_l_FloatQuat_of_RMat_2_max_1_
\n
{
\n
a_0 with
\n
F
9
_RealRMat_s_a01 = a_0.F
9
_RealRMat_s_a10 ;
\n
F
9
_RealRMat_s_a02 = a_0.F
9
_RealRMat_s_a20 ;
\n
F
9
_RealRMat_s_a10 = a_0.F
9
_RealRMat_s_a01 ;
\n
F
9
_RealRMat_s_a12 = a_0.F
9
_RealRMat_s_a21 ;
\n
F
9
_RealRMat_s_a20 = a_0.F
9
_RealRMat_s_a02 ;
\n
F
9
_RealRMat_s_a21 = a_0.F
9
_RealRMat_s_a12
\n
})"
,
"target"
:
"let a_0 = (L_l_RMat_of_FloatRMat Mf32_0 rm_0) in
\n
(L_l_FloatQuat_of_RMat_2_max_1_
\n
{
\n
a_0 with
\n
F
12
_RealRMat_s_a01 = a_0.F
12
_RealRMat_s_a10 ;
\n
F
12
_RealRMat_s_a02 = a_0.F
12
_RealRMat_s_a20 ;
\n
F
12
_RealRMat_s_a10 = a_0.F
12
_RealRMat_s_a01 ;
\n
F
12
_RealRMat_s_a12 = a_0.F
12
_RealRMat_s_a21 ;
\n
F
12
_RealRMat_s_a20 = a_0.F
12
_RealRMat_s_a02 ;
\n
F
12
_RealRMat_s_a21 = a_0.F
12
_RealRMat_s_a12
\n
})"
,
"pattern"
:
"L_l_FloatQuat_of_RMat_2_max_1_{RealRMat_s}"
},
"children"
:
{
"Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'"
:
[
{
"header"
:
"Definition"
,
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
10.5394
,
"steps"
:
1289
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
View file @
7ba71702
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
4
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_
6
rm_0)"
,
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
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"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
4
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F
6
_FloatRMat_m rm_0) in
\n
(P_rotation_matrix
\n
{
\n
F
9
_RealRMat_s_a00 = Mf32_
6
[(shift_float32 a_0 0)] ;
\n
F
9
_RealRMat_s_a01 = Mf32_
6
[(shift_float32 a_0 1)] ;
\n
F
9
_RealRMat_s_a02 = Mf32_
6
[(shift_float32 a_0 2)] ;
\n
F
9
_RealRMat_s_a10 = Mf32_
6
[(shift_float32 a_0 3)] ;
\n
F
9
_RealRMat_s_a11 = Mf32_
6
[(shift_float32 a_0 4)] ;
\n
F
9
_RealRMat_s_a12 = Mf32_
6
[(shift_float32 a_0 5)] ;
\n
F
9
_RealRMat_s_a20 = Mf32_
6
[(shift_float32 a_0 6)] ;
\n
F
9
_RealRMat_s_a21 = Mf32_
6
[(shift_float32 a_0 7)] ;
\n
F
9
_RealRMat_s_a22 = Mf32_
6
[(shift_float32 a_0 8)]
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F
9
_FloatRMat_m rm_0) in
\n
(P_rotation_matrix
\n
{
\n
F
12
_RealRMat_s_a00 = Mf32_
7
[(shift_float32 a_0 0)] ;
\n
F
12
_RealRMat_s_a01 = Mf32_
7
[(shift_float32 a_0 1)] ;
\n
F
12
_RealRMat_s_a02 = Mf32_
7
[(shift_float32 a_0 2)] ;
\n
F
12
_RealRMat_s_a10 = Mf32_
7
[(shift_float32 a_0 3)] ;
\n
F
12
_RealRMat_s_a11 = Mf32_
7
[(shift_float32 a_0 4)] ;
\n
F
12
_RealRMat_s_a12 = Mf32_
7
[(shift_float32 a_0 5)] ;
\n
F
12
_RealRMat_s_a20 = Mf32_
7
[(shift_float32 a_0 6)] ;
\n
F
12
_RealRMat_s_a21 = Mf32_
7
[(shift_float32 a_0 7)] ;
\n
F
12
_RealRMat_s_a22 = Mf32_
7
[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"P_rotation_matrix{RealRMat_s}[][]"
},
"children"
:
{
"Unfold 'P_rotation_matrix'"
:
[
{
"header"
:
"Definition"
,
...
...
@@ -17,10 +17,10 @@
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
4
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F
6
_FloatRMat_m rm_0) in
\n
(L_transpose
\n
{
\n
F
9
_RealRMat_s_a00 = Mf32_
6
[(shift_float32 a_0 0)] ;
\n
F
9
_RealRMat_s_a01 = Mf32_
6
[(shift_float32 a_0 1)] ;
\n
F
9
_RealRMat_s_a02 = Mf32_
6
[(shift_float32 a_0 2)] ;
\n
F
9
_RealRMat_s_a10 = Mf32_
6
[(shift_float32 a_0 3)] ;
\n
F
9
_RealRMat_s_a11 = Mf32_
6
[(shift_float32 a_0 4)] ;
\n
F
9
_RealRMat_s_a12 = Mf32_
6
[(shift_float32 a_0 5)] ;
\n
F
9
_RealRMat_s_a20 = Mf32_
6
[(shift_float32 a_0 6)] ;
\n
F
9
_RealRMat_s_a21 = Mf32_
6
[(shift_float32 a_0 7)] ;
\n
F
9
_RealRMat_s_a22 = Mf32_
6
[(shift_float32 a_0 8)]
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F
9
_FloatRMat_m rm_0) in
\n
(L_transpose
\n
{
\n
F
12
_RealRMat_s_a00 = Mf32_
7
[(shift_float32 a_0 0)] ;
\n
F
12
_RealRMat_s_a01 = Mf32_
7
[(shift_float32 a_0 1)] ;
\n
F
12
_RealRMat_s_a02 = Mf32_
7
[(shift_float32 a_0 2)] ;
\n
F
12
_RealRMat_s_a10 = Mf32_
7
[(shift_float32 a_0 3)] ;
\n
F
12
_RealRMat_s_a11 = Mf32_
7
[(shift_float32 a_0 4)] ;
\n
F
12
_RealRMat_s_a12 = Mf32_
7
[(shift_float32 a_0 5)] ;
\n
F
12
_RealRMat_s_a20 = Mf32_
7
[(shift_float32 a_0 6)] ;
\n
F
12
_RealRMat_s_a21 = Mf32_
7
[(shift_float32 a_0 7)] ;
\n
F
12
_RealRMat_s_a22 = Mf32_
7
[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"L_transpose{RealRMat_s}[][][][][]"
},
"children"
:
{
"Unfold 'L_transpose'"
:
...
...
@@ -29,14 +29,17 @@
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
4
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F
6
_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
F
9
_RealRMat_s_a00 = r_0 ;
\n
F
9
_RealRMat_s_a01 = r_1 ;
\n
F
9
_RealRMat_s_a02 = r_2 ;
\n
F
9
_RealRMat_s_a10 = r_3 ;
\n
F
9
_RealRMat_s_a11 = r_4 ;
\n
F
9
_RealRMat_s_a12 = r_5 ;
\n
F
9
_RealRMat_s_a20 = r_6 ;
\n
F
9
_RealRMat_s_a21 = r_7 ;
\n
F
9
_RealRMat_s_a22 = r_8
\n
}
\n
{
\n
F
9
_RealRMat_s_a00 = r_0 ;
\n
F
9
_RealRMat_s_a01 = r_3 ;
\n
F
9
_RealRMat_s_a02 = r_6 ;
\n
F
9
_RealRMat_s_a10 = r_1 ;
\n
F
9
_RealRMat_s_a11 = r_4 ;
\n
F
9
_RealRMat_s_a12 = r_7 ;
\n
F
9
_RealRMat_s_a20 = r_2 ;
\n
F
9
_RealRMat_s_a21 = r_5 ;
\n
F
9
_RealRMat_s_a22 = r_8
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F
9
_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
F
12
_RealRMat_s_a00 = r_0 ;
\n
F
12
_RealRMat_s_a01 = r_1 ;
\n
F
12
_RealRMat_s_a02 = r_2 ;
\n
F
12
_RealRMat_s_a10 = r_3 ;
\n
F
12
_RealRMat_s_a11 = r_4 ;
\n
F
12
_RealRMat_s_a12 = r_5 ;
\n
F
12
_RealRMat_s_a20 = r_6 ;
\n
F
12
_RealRMat_s_a21 = r_7 ;
\n
F
12
_RealRMat_s_a22 = r_8
\n
}
\n
{
\n
F
12
_RealRMat_s_a00 = r_0 ;
\n
F
12
_RealRMat_s_a01 = r_3 ;
\n
F
12
_RealRMat_s_a02 = r_6 ;
\n
F
12
_RealRMat_s_a10 = r_1 ;
\n
F
12
_RealRMat_s_a11 = r_4 ;
\n
F
12
_RealRMat_s_a12 = r_7 ;
\n
F
12
_RealRMat_s_a20 = r_2 ;
\n
F
12
_RealRMat_s_a21 = r_5 ;
\n
F
12
_RealRMat_s_a22 = r_8
\n
})"
,
"pattern"
:
"L_mult_RealRMat{RealRMat_s}{RealRMat_s}"
},
"children"
:
{
"Unfold 'L_mult_RealRMat'"
:
[
{
"header"
:
"Definition"
,
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
0.32
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_11.json
0 → 100644
View file @
7ba71702
[
{
"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)"
,
"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_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"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"L_id_rmat"
,
"pattern"
:
"L_id_rmat"
},
"children"
:
{
"Unfold 'L_id_rmat'"
:
[
{
"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_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'"
:
[
{
"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_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'"
:
[
{
"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_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'"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
5.56
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_12.json
View file @
7ba71702
[
{
"prover"
:
"script"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
[
{
"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"
:
"clause-goal"
,
"target"
:
"let a_0 = (shiftfield_F6_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_F4_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_F4_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_F4_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_quaterion
\n
m_2[(shiftfield_F4_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_quaterion[=]$q[=]shiftfield_F4_FloatQuat_qz"
},
"children"
:
{
"Unfold 'P_unary_quaterion'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
2
,
"target"
:
"(shift_float32 (shiftfield_F6_FloatRMat_m rm_0) 8)"
,
"pattern"
:
"shift_float32shiftfield_F6_FloatRMat_m"
},
"children"
:
{
"Unfold 'shift_float32'"
:
"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"
:
1
0
.
},
"time"
:
1
5
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
1
0
.
},
"time"
:
1
5
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
"time"
:
15
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
1
0
.
},
"time"
:
1
5
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
}
]
}
}
]
}
}
]
"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
0 → 100644
View file @
7ba71702
[
{
"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_19[(shift_float32 a_0 4)]<Mf32_19[(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
},
{
"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"
:
2.69
}
],
"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"
,
"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)]"
,