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
704419ec
Commit
704419ec
authored
May 06, 2021
by
POLLIEN Baptiste
Browse files
Removing assertions
parent
b7b55dd7
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
9 additions
and
11 deletions
+9
-11
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
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_321_ensures_2.json
...frama-c/wp/script/float_rmat_of_eulers_321_ensures_2.json
+1
-1
sw/airborne/math/pprz_algebra_float.c
sw/airborne/math/pprz_algebra_float.c
+0
-2
No files found.
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_321_ensures.json
View file @
704419ec
...
...
@@ -59,30 +59,30 @@
{
"Goal 1/6"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
1.4
375
,
"time"
:
1.4
602
,
"steps"
:
102
}
],
"Goal 2/6"
:
[
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"valid"
,
"time"
:
0.
66
,
"steps"
:
241
4090
}
],
"time"
:
0.
45
,
"steps"
:
241
7925
}
],
"Goal 3/6"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
2.
4657
,
"time"
:
2.
0874
,
"steps"
:
102
}
],
"Goal 4/6"
:
[
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"valid"
,
"time"
:
0.5
6
,
"steps"
:
241
4075
}
],
"time"
:
0.5
5
,
"steps"
:
241
7912
}
],
"Goal 5/6"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
2.2
32
4
,
"time"
:
1.6
32
,
"steps"
:
102
}
],
"Goal 6/6"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
2.0
37
1
,
"time"
:
1.59
37
,
"steps"
:
102
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_321_ensures_2.json
View file @
704419ec
...
...
@@ -11,5 +11,5 @@
"children"
:
{
"Unfold 'P_special_orthogonal'"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
2.1
12
5
,
"time"
:
1.8
12
7
,
"steps"
:
102
}
]
}
}
]
}
}
]
sw/airborne/math/pprz_algebra_float.c
View file @
704419ec
...
...
@@ -193,9 +193,7 @@ void float_rmat_of_axis_angle(struct FloatRMat *rm, struct FloatVect3 *uv, float
void
float_rmat_of_eulers_321
(
struct
FloatRMat
*
rm
,
struct
FloatEulers
*
e
)
{
const
float
sphi
=
sinf
(
e
->
phi
);
//@ assert sphi == \sin(e->phi);
const
float
cphi
=
cosf
(
e
->
phi
);
//@assert cphi == \cos(e->phi);
const
float
stheta
=
sinf
(
e
->
theta
);
const
float
ctheta
=
cosf
(
e
->
theta
);
const
float
spsi
=
sinf
(
e
->
psi
);
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment