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
19613b16
Commit
19613b16
authored
Apr 21, 2021
by
POLLIEN Baptiste
Browse files
Fix name for unary quaternion
parent
b1951d7f
Changes
36
Hide whitespace changes
Inline
Side-by-side
Showing
20 changed files
with
377 additions
and
56 deletions
+377
-56
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
+4
-4
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
+4
-4
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
+17
-4
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
+1
-1
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
+8
-7
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
+28
-7
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
-7
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
+5
-5
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
+30
-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
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
+3
-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
+43
-0
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_22.json
...orne/.frama-c/wp/script/float_quat_of_rmat_assert_22.json
+2
-0
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_24.json
...orne/.frama-c/wp/script/float_quat_of_rmat_assert_24.json
+2
-0
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_ensures.json
...rborne/.frama-c/wp/script/float_quat_of_rmat_ensures.json
+13
-13
No files found.
sw/airborne/.frama-c/wp/interactive/lemma_float_rmat_of_eulers_321_1.v
View file @
19613b16
...
...
@@ -502,7 +502,7 @@ Definition L_l_RMat_of_FloatQuat_bis_1 (Mf32:addr -> Reals.Rdefinitions.R)
(
2
%
R
*
(
r11
+
r12
)
%
R
)
%
R
(
1
%
R
+
((
-
1
%
R
)
%
R
*
(
2
%
R
*
(
r10
+
r1
)
%
R
)
%
R
)
%
R
)
%
R
.
(
*
Why3
assumption
*
)
Definition
P_unary_quaterion
(
Mf32
:
addr
->
Reals
.
Rdefinitions
.
R
)
(
q
:
addr
)
:
Definition
P_unary_quater
n
ion
(
Mf32
:
addr
->
Reals
.
Rdefinitions
.
R
)
(
q
:
addr
)
:
Prop
:=
let
r
:=
Mf32
(
shift
q
0
%
Z
)
in
let
r1
:=
Mf32
(
shift
q
1
%
Z
)
in
...
...
@@ -565,21 +565,21 @@ Axiom Q_mult_rmat_id_neutral :
Axiom
Q_mutliple_def_rmat_of_quat_1
:
forall
(
Malloc
:
Numbers
.
BinNums
.
Z
->
Numbers
.
BinNums
.
Z
)
(
Mf32
:
addr
->
Reals
.
Rdefinitions
.
R
)
(
q
:
addr
),
P_unary_quaterion
Mf32
q
->
valid_rd
Malloc
q
4
%
Z
->
P_unary_quater
n
ion
Mf32
q
->
valid_rd
Malloc
q
4
%
Z
->
EqS12_RealRMat_s
(
L_l_RMat_of_FloatQuat
Mf32
q
)
(
L_l_RMat_of_FloatQuat_bis_1
Mf32
q
).
Axiom
Q_mutliple_def_rmat_of_quat_2
:
forall
(
Malloc
:
Numbers
.
BinNums
.
Z
->
Numbers
.
BinNums
.
Z
)
(
Mf32
:
addr
->
Reals
.
Rdefinitions
.
R
)
(
q
:
addr
),
P_unary_quaterion
Mf32
q
->
valid_rd
Malloc
q
4
%
Z
->
P_unary_quater
n
ion
Mf32
q
->
valid_rd
Malloc
q
4
%
Z
->
EqS12_RealRMat_s
(
L_l_RMat_of_FloatQuat
Mf32
q
)
(
L_l_RMat_of_FloatQuat_bis_2
Mf32
q
).
Axiom
Q_mutliple_def_rmat_of_quat_3
:
forall
(
Malloc
:
Numbers
.
BinNums
.
Z
->
Numbers
.
BinNums
.
Z
)
(
Mf32
:
addr
->
Reals
.
Rdefinitions
.
R
)
(
q
:
addr
),
P_unary_quaterion
Mf32
q
->
valid_rd
Malloc
q
4
%
Z
->
P_unary_quater
n
ion
Mf32
q
->
valid_rd
Malloc
q
4
%
Z
->
EqS12_RealRMat_s
(
L_l_RMat_of_FloatQuat_bis_1
Mf32
q
)
(
L_l_RMat_of_FloatQuat_bis_2
Mf32
q
).
...
...
sw/airborne/.frama-c/wp/interactive/lemma_float_rmat_of_eulers_321_2.v
View file @
19613b16
...
...
@@ -515,7 +515,7 @@ Definition L_l_RMat_of_FloatQuat_bis_1 (Mf32:addr -> Reals.Rdefinitions.R)
(
2
%
R
*
(
r11
+
r12
)
%
R
)
%
R
(
1
%
R
+
((
-
1
%
R
)
%
R
*
(
2
%
R
*
(
r10
+
r1
)
%
R
)
%
R
)
%
R
)
%
R
.
(
*
Why3
assumption
*
)
Definition
P_unary_quaterion
(
Mf32
:
addr
->
Reals
.
Rdefinitions
.
R
)
(
q
:
addr
)
:
Definition
P_unary_quater
n
ion
(
Mf32
:
addr
->
Reals
.
Rdefinitions
.
R
)
(
q
:
addr
)
:
Prop
:=
let
r
:=
Mf32
(
shift
q
0
%
Z
)
in
let
r1
:=
Mf32
(
shift
q
1
%
Z
)
in
...
...
@@ -578,21 +578,21 @@ Axiom Q_mult_rmat_id_neutral :
Axiom
Q_mutliple_def_rmat_of_quat_1
:
forall
(
Malloc
:
Numbers
.
BinNums
.
Z
->
Numbers
.
BinNums
.
Z
)
(
Mf32
:
addr
->
Reals
.
Rdefinitions
.
R
)
(
q
:
addr
),
P_unary_quaterion
Mf32
q
->
valid_rd
Malloc
q
4
%
Z
->
P_unary_quater
n
ion
Mf32
q
->
valid_rd
Malloc
q
4
%
Z
->
EqS12_RealRMat_s
(
L_l_RMat_of_FloatQuat
Mf32
q
)
(
L_l_RMat_of_FloatQuat_bis_1
Mf32
q
).
Axiom
Q_mutliple_def_rmat_of_quat_2
:
forall
(
Malloc
:
Numbers
.
BinNums
.
Z
->
Numbers
.
BinNums
.
Z
)
(
Mf32
:
addr
->
Reals
.
Rdefinitions
.
R
)
(
q
:
addr
),
P_unary_quaterion
Mf32
q
->
valid_rd
Malloc
q
4
%
Z
->
P_unary_quater
n
ion
Mf32
q
->
valid_rd
Malloc
q
4
%
Z
->
EqS12_RealRMat_s
(
L_l_RMat_of_FloatQuat
Mf32
q
)
(
L_l_RMat_of_FloatQuat_bis_2
Mf32
q
).
Axiom
Q_mutliple_def_rmat_of_quat_3
:
forall
(
Malloc
:
Numbers
.
BinNums
.
Z
->
Numbers
.
BinNums
.
Z
)
(
Mf32
:
addr
->
Reals
.
Rdefinitions
.
R
)
(
q
:
addr
),
P_unary_quaterion
Mf32
q
->
valid_rd
Malloc
q
4
%
Z
->
P_unary_quater
n
ion
Mf32
q
->
valid_rd
Malloc
q
4
%
Z
->
EqS12_RealRMat_s
(
L_l_RMat_of_FloatQuat_bis_1
Mf32
q
)
(
L_l_RMat_of_FloatQuat_bis_2
Mf32
q
).
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
View file @
19613b16
...
...
@@ -44,5 +44,5 @@
{
"Unfold 'L_l_Quat_of_FloatQuat'"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
9.5682
,
"time"
:
11.8791
,
"steps"
:
1715
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
View file @
19613b16
...
...
@@ -22,10 +22,23 @@
"pattern"
:
"L_l_FloatQuat_of_RMat_1_max_1_{RealRMat_s}"
},
"children"
:
{
"Unfold 'L_l_FloatQuat_of_RMat_1_max_1_'"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
8.7286
,
"steps"
:
1690
},
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
View file @
19613b16
...
...
@@ -58,7 +58,7 @@
{
"Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
2.96
,
"time"
:
3.8529
,
"steps"
:
1275
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
View file @
19613b16
...
...
@@ -38,7 +38,7 @@
{
"Unfold 'L_mult_RealRMat'"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
0.
25
},
"time"
:
0.
38
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_11.json
0 → 100644
View file @
19613b16
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_6 rm_0)"
,
"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_6[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_6[(shift_float32 a_0 8)]
\n
})"
,
"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_6[(shift_float32 a_0 0)] ;
\n
F12_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;
\n
F12_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;
\n
F12_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;
\n
F12_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;
\n
F12_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;
\n
F12_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;
\n
F12_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;
\n
F12_RealRMat_s_a22 = Mf32_6[(shift_float32 a_0 8)]
\n
})"
,
"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_6[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_6[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_6[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_6[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_6[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_6[(shift_float32 a_0 5)] in
\n
let r_6 = Mf32_6[(shift_float32 a_0 6)] in
\n
let r_7 = Mf32_6[(shift_float32 a_0 7)] in
\n
let r_8 = Mf32_6[(shift_float32 a_0 8)] in
\n
(L_mult_RealRMat
\n
{
\n
F12_RealRMat_s_a00 = r_0 ;
\n
F12_RealRMat_s_a01 = r_1 ;
\n
F12_RealRMat_s_a02 = r_2 ;
\n
F12_RealRMat_s_a10 = r_3 ;
\n
F12_RealRMat_s_a11 = r_4 ;
\n
F12_RealRMat_s_a12 = r_5 ;
\n
F12_RealRMat_s_a20 = r_6 ;
\n
F12_RealRMat_s_a21 = r_7 ;
\n
F12_RealRMat_s_a22 = r_8
\n
}
\n
{
\n
F12_RealRMat_s_a00 = r_0 ;
\n
F12_RealRMat_s_a01 = r_3 ;
\n
F12_RealRMat_s_a02 = r_6 ;
\n
F12_RealRMat_s_a10 = r_1 ;
\n
F12_RealRMat_s_a11 = r_4 ;
\n
F12_RealRMat_s_a12 = r_7 ;
\n
F12_RealRMat_s_a20 = r_2 ;
\n
F12_RealRMat_s_a21 = r_5 ;
\n
F12_RealRMat_s_a22 = r_8
\n
})"
,
"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_6[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_6[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_6[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_6[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_6[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_6[(shift_float32 a_0 5)] in
\n
let r_6 = ((r_0*r_3)+(r_1*r_4)+(r_2*r_5)) in
\n
let r_7 = Mf32_6[(shift_float32 a_0 6)] in
\n
let r_8 = Mf32_6[(shift_float32 a_0 7)] in
\n
let r_9 = Mf32_6[(shift_float32 a_0 8)] in
\n
let r_10 = ((r_0*r_7)+(r_1*r_8)+(r_2*r_9)) in
\n
let r_11 = ((r_3*r_7)+(r_4*r_8)+(r_5*r_9)) in
\n
(EqS12_RealRMat_s
\n
{
\n
F12_RealRMat_s_a00 = (r_0*r_0)+(r_1*r_1)+(r_2*r_2) ;
\n
F12_RealRMat_s_a01 = r_6 ;
\n
F12_RealRMat_s_a02 = r_10 ;
\n
F12_RealRMat_s_a10 = r_6 ;
\n
F12_RealRMat_s_a11 = (r_3*r_3)+(r_4*r_4)+(r_5*r_5) ;
\n
F12_RealRMat_s_a12 = r_11 ;
\n
F12_RealRMat_s_a20 = r_10 ;
\n
F12_RealRMat_s_a21 = r_11 ;
\n
F12_RealRMat_s_a22 = (r_7*r_7)+(r_8*r_8)+(r_9*r_9)
\n
}
\n
{
\n
F12_RealRMat_s_a00 = 1 ;
\n
F12_RealRMat_s_a01 = 0 ;
\n
F12_RealRMat_s_a02 = 0 ;
\n
F12_RealRMat_s_a10 = 0 ;
\n
F12_RealRMat_s_a11 = 1 ;
\n
F12_RealRMat_s_a12 = 0 ;
\n
F12_RealRMat_s_a20 = 0 ;
\n
F12_RealRMat_s_a21 = 0 ;
\n
F12_RealRMat_s_a22 = 1
\n
})"
,
"pattern"
:
"EqS12_RealRMat_s{RealRMat_s}{RealRMat_s}"
},
"children"
:
{
"Unfold 'EqS12_RealRMat_s'"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
5.89
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_12.json
View file @
19613b16
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
}
]
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-goal"
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 =
\n
(
\\
sqrt
\n
(1+Mf32_6[(shift_float32 a_0 0)]+Mf32_6[(shift_float32 a_0 4)]+
\n
Mf32_6[(shift_float32 a_0 8)])) in
\n
let m_0 = Mf32_6[(shiftfield_F7_FloatQuat_qi q_1)->1/2*r_0] in
\n
let r_1 = (2*r_0) in
\n
let m_1 =
\n
m_0[(shiftfield_F7_FloatQuat_qx q_1)
\n
->(m_0[(shift_float32 a_0 5)]-m_0[(shift_float32 a_0 7)]) div r_1] in
\n
let m_2 =
\n
m_1[(shiftfield_F7_FloatQuat_qy q_1)
\n
->(m_1[(shift_float32 a_0 6)]-m_1[(shift_float32 a_0 2)]) div r_1] in
\n
(P_unary_quaternion
\n
m_2[(shiftfield_F7_FloatQuat_qz q_1)
\n
->(m_2[(shift_float32 a_0 1)]-m_2[(shift_float32 a_0 3)]) div r_1] q_1)"
,
"pattern"
:
"P_unary_quaternion[=]$q[=]shiftfield_F7_FloatQuat_qz"
},
"children"
:
{
"Unfold 'P_unary_quaternion'"
:
[
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"valid"
,
"time"
:
1.55
,
"steps"
:
2791404
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_13.json
View file @
19613b16
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
}
]
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"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.1
}
],
"Else"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
8.12
}
]
}
}
],
"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.74
}
],
"Else"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
3.43
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_14.json
View file @
19613b16
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
}
]
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"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.0265
,
"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"
:
10
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"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.02
}
],
"Else"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
2.78
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_15.json
View file @
19613b16
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
1
0
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
1
0
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
1
0
.
},
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
1
5
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
1
5
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
1
5
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
1
0
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
1
0
.
}
]
"verdict"
:
"timeout"
,
"time"
:
1
5
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
1
5
.
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_16.json
0 → 100644
View file @
19613b16
[
{
"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"
:
4.81
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
3.1779
,
"steps"
:
1003
}
]
}
}
],
"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"
:
4.82
}
],
"Else"
:
[
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
0.54
,
"steps"
:
386202
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_17.json
0 → 100644
View file @
19613b16
[
{
"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"
:
6.2
}
],
"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"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.0298
,
"steps"
:
28
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
1.6341
,
"steps"
:
719
}
]
}
}
]
}
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
4.2455
,
"steps"
:
1533
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_18.json
0 → 100644
View file @
19613b16
[
{
"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"
:
5.7
}
],
"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.08
,
"steps"
:
186302
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
1.6261
,
"steps"
:
721
}
]
}
}
]
}
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
5.1298
,
"steps"
:
1537
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_19.json
0 → 100644
View file @
19613b16
[
{
"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"
:
2.52
}
],
"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"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.0304
,
"steps"
:
28
}
],
"Else"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
5.1
}
]
}
}
]
}
}
],
"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"
:
4.24
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
1.6757
,
"steps"
:
723
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_2.json
View file @
19613b16
...
...
@@ -48,9 +48,10 @@
"pattern"
:
"L_mult_RealRMat{RealRMat_s}{RealRMat_s}"
},
"children"
:
{
"Unfold 'L_mult_RealRMat'"
:
[
{
"prover"
:
"
CVC4:1.9-prerelease:strings+
counterexamples"
,
[
{
"prover"
:
"
Z3:4.8.6:
counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
9.1
},
"time"
:
0.55
,
"steps"
:
538468
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_20.json
0 → 100644
View file @
19613b16
[
{
"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.56
}
],
"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"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.0414
,
"steps"
:
28
}
],
"Else"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
3.36
}
]
}
}
]
}
}
],
"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"
:
4.89
}
],
"Else"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
2.1687
,
"steps"
:
728
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_22.json
0 → 100644
View file @
19613b16
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
8.4405
,
"steps"
:
3757
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_24.json
0 → 100644
View file @
19613b16
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
: