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
c6163b37
Commit
c6163b37
authored
Apr 15, 2021
by
POLLIEN Baptiste
Browse files
Coq proof lemma
parent
59aaa4f1
Changes
9
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
9 changed files
with
934 additions
and
44 deletions
+934
-44
sw/airborne/.frama-c/wp/interactive/lemma_float_rmat_of_eulers_321.v
.../.frama-c/wp/interactive/lemma_float_rmat_of_eulers_321.v
+681
-0
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_321_ensures.json
.../.frama-c/wp/script/float_rmat_of_eulers_321_ensures.json
+109
-6
sw/airborne/.frama-c/wp/script/lemma_float_rmat_of_eulers_321.json
...ne/.frama-c/wp/script/lemma_float_rmat_of_eulers_321.json
+6
-0
sw/airborne/math/libc_frama_c.h
sw/airborne/math/libc_frama_c.h
+64
-0
sw/airborne/math/pprz_algebra_float.c
sw/airborne/math/pprz_algebra_float.c
+65
-0
sw/airborne/math/pprz_algebra_float.h
sw/airborne/math/pprz_algebra_float.h
+2
-0
sw/airborne/math/pprz_algebra_float_convert_rmat_frama_c.h
sw/airborne/math/pprz_algebra_float_convert_rmat_frama_c.h
+1
-3
sw/airborne/math/pprz_algebra_float_frama_c.h
sw/airborne/math/pprz_algebra_float_frama_c.h
+2
-0
sw/airborne/math/pprz_algebra_int_frama_c.h
sw/airborne/math/pprz_algebra_int_frama_c.h
+4
-35
No files found.
sw/airborne/.frama-c/wp/interactive/lemma_float_rmat_of_eulers_321.v
0 → 100644
View file @
c6163b37
This diff is collapsed.
Click to expand it.
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_321_ensures.json
View file @
c6163b37
[
{
"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"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
}
]
[
{
"prover"
:
"script"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
,
"steps"
:
2332912
},
{
"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_9[(shiftfield_F10_FloatEulers_psi e_1)] in
\n
let r_1 = (
\\
cos r_0) in
\n
let r_2 = Mf32_9[(shiftfield_F10_FloatEulers_theta e_1)] in
\n
let r_3 = (
\\
cos r_2) in
\n
let r_4 = (
\\
sin r_0) in
\n
let r_5 = (
\\
sin r_2) in
\n
let r_6 = Mf32_9[(shiftfield_F10_FloatEulers_phi e_1)] in
\n
let r_7 = (
\\
cos r_6) in
\n
let r_8 = (
\\
sin r_6) in
\n
(L_l_RMat_of_FloatRMat
\n
Mf32_9[(shift_float32 a_0 0)->r_1*r_3][(shift_float32 a_0 1)->r_4*r_3]
\n
[(shift_float32 a_0 2)->-r_5][(shift_float32 a_0 3)
\n
->(r_8*r_5*r_1)-(r_4*r_7)][(shift_float32 a_0 4)
\n
->(r_7*r_1)+(r_8*r_4*r_5)][(shift_float32 a_0 5)->r_8*r_3]
\n
[(shift_float32 a_0 6)->(r_8*r_4)+(r_5*r_7*r_1)][(shift_float32 a_0 7)
\n
->(r_4*r_5*r_7)-(r_8*r_1)][(shift_float32 a_0 8)->r_7*r_3] rm_0)"
,
"pattern"
:
"L_l_RMat_of_FloatRMat[=]$rm[=]shift_float32"
},
"children"
:
{
"Unfold 'L_l_RMat_of_FloatRMat'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-goal"
,
"target"
:
"let r_0 = Mf32_9[(shiftfield_F10_FloatEulers_psi e_1)] in
\n
let r_1 = (
\\
cos r_0) in
\n
let r_2 = Mf32_9[(shiftfield_F10_FloatEulers_theta e_1)] in
\n
let r_3 = (
\\
cos r_2) in
\n
let r_4 = (
\\
sin r_0) in
\n
let r_5 = (
\\
sin r_2) in
\n
let r_6 = Mf32_9[(shiftfield_F10_FloatEulers_phi e_1)] in
\n
let r_7 = (
\\
cos r_6) in
\n
let r_8 = (
\\
sin r_6) in
\n
(P_rotation_matrix
\n
{
\n
F12_RealRMat_s_a00 = r_1*r_3 ;
\n
F12_RealRMat_s_a01 = r_4*r_3 ;
\n
F12_RealRMat_s_a02 = -r_5 ;
\n
F12_RealRMat_s_a10 = (r_8*r_5*r_1)-(r_4*r_7) ;
\n
F12_RealRMat_s_a11 = (r_7*r_1)+(r_8*r_4*r_5) ;
\n
F12_RealRMat_s_a12 = r_8*r_3 ;
\n
F12_RealRMat_s_a20 = (r_8*r_4)+(r_5*r_7*r_1) ;
\n
F12_RealRMat_s_a21 = (r_4*r_5*r_7)-(r_8*r_1) ;
\n
F12_RealRMat_s_a22 = r_7*r_3
\n
})"
,
"pattern"
:
"P_rotation_matrix{RealRMat_s}**.-1"
},
"children"
:
{
"Unfold 'P_rotation_matrix'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"let r_0 = Mf32_9[(shiftfield_F10_FloatEulers_psi e_1)] in
\n
let r_1 = (
\\
cos r_0) in
\n
let r_2 = Mf32_9[(shiftfield_F10_FloatEulers_theta e_1)] in
\n
let r_3 = (
\\
cos r_2) in
\n
let r_4 = (
\\
sin r_0) in
\n
let r_5 = (
\\
sin r_2) in
\n
let r_6 = Mf32_9[(shiftfield_F10_FloatEulers_phi e_1)] in
\n
let r_7 = (
\\
cos r_6) in
\n
let r_8 = (
\\
sin r_6) in
\n
(L_transpose
\n
{
\n
F12_RealRMat_s_a00 = r_1*r_3 ;
\n
F12_RealRMat_s_a01 = r_4*r_3 ;
\n
F12_RealRMat_s_a02 = -r_5 ;
\n
F12_RealRMat_s_a10 = (r_8*r_5*r_1)-(r_4*r_7) ;
\n
F12_RealRMat_s_a11 = (r_7*r_1)+(r_8*r_4*r_5) ;
\n
F12_RealRMat_s_a12 = r_8*r_3 ;
\n
F12_RealRMat_s_a20 = (r_8*r_4)+(r_5*r_7*r_1) ;
\n
F12_RealRMat_s_a21 = (r_4*r_5*r_7)-(r_8*r_1) ;
\n
F12_RealRMat_s_a22 = r_7*r_3
\n
})"
,
"pattern"
:
"L_transpose{RealRMat_s}**.-1++*+"
},
"children"
:
{
"Unfold 'L_transpose'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"L_id_rmat"
,
"pattern"
:
"L_id_rmat"
},
"children"
:
{
"Unfold 'L_id_rmat'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"let r_0 = Mf32_9[(shiftfield_F10_FloatEulers_psi e_1)] in
\n
let r_1 = (
\\
cos r_0) in
\n
let r_2 = Mf32_9[(shiftfield_F10_FloatEulers_theta e_1)] in
\n
let r_3 = (
\\
cos r_2) in
\n
let r_4 = (r_1*r_3) in
\n
let r_5 = (
\\
sin r_0) in
\n
let r_6 = (r_5*r_3) in
\n
let r_7 = (
\\
sin r_2) in
\n
let r_8 = (-r_7) in
\n
let r_9 = Mf32_9[(shiftfield_F10_FloatEulers_phi e_1)] in
\n
let r_10 = (
\\
cos r_9) in
\n
let r_11 = (
\\
sin r_9) in
\n
let r_12 = ((r_11*r_7*r_1)-(r_5*r_10)) in
\n
let r_13 = ((r_10*r_1)+(r_11*r_5*r_7)) in
\n
let r_14 = (r_11*r_3) in
\n
let r_15 = ((r_11*r_5)+(r_7*r_10*r_1)) in
\n
let r_16 = ((r_5*r_7*r_10)-(r_11*r_1)) in
\n
let r_17 = (r_10*r_3) in
\n
(L_mult_RealRMat
\n
{
\n
F12_RealRMat_s_a00 = r_4 ;
\n
F12_RealRMat_s_a01 = r_6 ;
\n
F12_RealRMat_s_a02 = r_8 ;
\n
F12_RealRMat_s_a10 = r_12 ;
\n
F12_RealRMat_s_a11 = r_13 ;
\n
F12_RealRMat_s_a12 = r_14 ;
\n
F12_RealRMat_s_a20 = r_15 ;
\n
F12_RealRMat_s_a21 = r_16 ;
\n
F12_RealRMat_s_a22 = r_17
\n
}
\n
{
\n
F12_RealRMat_s_a00 = r_4 ;
\n
F12_RealRMat_s_a01 = r_12 ;
\n
F12_RealRMat_s_a02 = r_15 ;
\n
F12_RealRMat_s_a10 = r_6 ;
\n
F12_RealRMat_s_a11 = r_13 ;
\n
F12_RealRMat_s_a12 = r_16 ;
\n
F12_RealRMat_s_a20 = r_8 ;
\n
F12_RealRMat_s_a21 = r_14 ;
\n
F12_RealRMat_s_a22 = r_17
\n
})"
,
"pattern"
:
"L_mult_RealRMat{RealRMat_s}{RealRMat_s}"
},
"children"
:
{
"Unfold 'L_mult_RealRMat'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-goal"
,
"target"
:
"let r_0 = Mf32_9[(shiftfield_F10_FloatEulers_theta e_1)] in
\n
let r_1 = (
\\
sin r_0) in
\n
let r_2 = Mf32_9[(shiftfield_F10_FloatEulers_psi e_1)] in
\n
let r_3 = (
\\
sin r_2) in
\n
let r_4 = (
\\
cos r_0) in
\n
let r_5 = (
\\
cos r_2) in
\n
let r_6 = Mf32_9[(shiftfield_F10_FloatEulers_phi e_1)] in
\n
let r_7 = (
\\
sin r_6) in
\n
let r_8 = (
\\
cos r_6) in
\n
let r_9 = ((r_8*r_5)+(r_7*r_3*r_1)) in
\n
let r_10 = ((r_7*r_1*r_5)-(r_3*r_8)) in
\n
let r_11 = ((-1*r_7*r_1*r_4)+(r_3*r_4*r_9)+(r_5*r_4*r_10)) in
\n
let r_12 = ((r_3*r_1*r_8)-(r_7*r_5)) in
\n
let r_13 = ((r_7*r_3)+(r_1*r_8*r_5)) in
\n
let r_14 = ((-1*r_1*r_8*r_4)+(r_3*r_4*r_12)+(r_5*r_4*r_13)) in
\n
let r_15 = ((r_7*r_8*r_4*r_4)+(r_12*r_9)+(r_10*r_13)) in
\n
(EqS12_RealRMat_s
\n
{
\n
F12_RealRMat_s_a00 = (r_1*r_1)+(r_3*r_3*r_4*r_4)+(r_5*r_5*r_4*r_4) ;
\n
F12_RealRMat_s_a01 = r_11 ;
\n
F12_RealRMat_s_a02 = r_14 ;
\n
F12_RealRMat_s_a10 = r_11 ;
\n
F12_RealRMat_s_a11 = (r_7*r_7*r_4*r_4)+(r_10*r_10)+(r_9*r_9) ;
\n
F12_RealRMat_s_a12 = r_15 ;
\n
F12_RealRMat_s_a20 = r_14 ;
\n
F12_RealRMat_s_a21 = r_15 ;
\n
F12_RealRMat_s_a22 = (r_8*r_8*r_4*r_4)+(r_12*r_12)+(r_13*r_13)
\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'"
:
[
{
"header"
:
"Split"
,
"tactic"
:
"Wp.split"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-goal"
,
"target"
:
"let r_0 = Mf32_9[(shiftfield_F10_FloatEulers_theta e_1)] in
\n
let r_1 = (
\\
sin r_0) in
\n
let r_2 = Mf32_9[(shiftfield_F10_FloatEulers_psi e_1)] in
\n
let r_3 = (
\\
sin r_2) in
\n
let r_4 = (
\\
cos r_0) in
\n
let r_5 = (
\\
cos r_2) in
\n
let r_6 = Mf32_9[(shiftfield_F10_FloatEulers_phi e_1)] in
\n
let r_7 = (
\\
sin r_6) in
\n
let r_8 = (
\\
cos r_6) in
\n
let r_9 = ((r_7*r_1*r_5)-(r_3*r_8)) in
\n
let r_10 = ((r_8*r_5)+(r_7*r_3*r_1)) in
\n
let r_11 = ((r_3*r_1*r_8)-(r_7*r_5)) in
\n
let r_12 = ((r_7*r_3)+(r_1*r_8*r_5)) in
\n
(((r_1*r_1)+(r_3*r_3*r_4*r_4)+(r_5*r_5*r_4*r_4))=1)
\n
/
\\
(((r_7*r_7*r_4*r_4)+(r_9*r_9)+(r_10*r_10))=1)
\n
/
\\
(((r_7*r_8*r_4*r_4)+(r_11*r_10)+(r_9*r_12))=0)
\n
/
\\
(((r_8*r_8*r_4*r_4)+(r_11*r_11)+(r_12*r_12))=1)
\n
/
\\
(((-1*r_7*r_1*r_4)+(r_3*r_4*r_10)+(r_5*r_4*r_9))=0)
\n
/
\\
(((-1*r_1*r_8*r_4)+(r_3*r_4*r_11)+(r_5*r_4*r_12))=0)"
,
"pattern"
:
"&======+1+1+0+1+0+0*************"
},
"children"
:
{
"Goal 1/6"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.5
,
"steps"
:
102
}
],
"Goal 2/6"
:
[
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"valid"
,
"time"
:
0.48
,
"steps"
:
2332912
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
}
],
"Goal 3/6"
:
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
1.1626
,
"steps"
:
102
}
],
"Goal 4/6"
:
[
{
"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"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
}
],
"Goal 5/6"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.6993
,
"steps"
:
102
}
],
"Goal 6/6"
:
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
0.7479
,
"steps"
:
102
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/lemma_float_rmat_of_eulers_321.json
0 → 100644
View file @
c6163b37
[
{
"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"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
}
]
sw/airborne/math/libc_frama_c.h
0 → 100644
View file @
c6163b37
#ifndef LIBC_FRAMA_C_H
#define LIBC_FRAMA_C_H
#ifdef __cplusplus
extern
"C"
{
#endif
#include <limits.h>
#include <stdlib.h>
#define PI2 1.5707963
/****************************************************
* Redefinition of the contract of libC functions
* **************************************************/
/*@ requires finite_arg: \is_finite(x);
assigns \result \from x;
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. <= \result <= 1.;
ensures result_value: \result == \cos(x);
*/
extern
float
cosf
(
float
x
);
/*@ requires finite_arg: \is_finite(x);
assigns \result \from x;
ensures finite_result: \is_finite(\result);
ensures result_domain: -1. <= \result <= 1.;
ensures result_value: \result == \sin(x);
*/
extern
float
sinf
(
float
x
);
/*@ requires finite_args: \is_finite(x) && \is_finite(y);
requires finite_logic_result: \is_finite(atan2f(x, y));
assigns \result \from x, y;
ensures finite_result: \is_finite(\result);
ensures -PI2 <= \result <= PI2;
*/
extern
float
atan2f
(
float
y
,
float
x
);
/*@ requires in_domain: \is_finite(x) && \abs(x) <= 1;
assigns \result \from x;
ensures finite_result: \is_finite(\result);
ensures -PI2 <= \result <= PI2;
*/
extern
float
asinf
(
float
x
);
/*
typedef struct __fc_lldiv_t {
long long int quot; / Quotient. /
long long int rem; / Remainder. /
} lldiv_t;
*/
/*@ assigns \result \from numer, denom;
ensures \result.quot == numer / denom;
ensures \result.rem == numer % denom; */
extern
lldiv_t
lldiv
(
long
long
int
numer
,
long
long
int
denom
);
#ifdef __cplusplus
}
/* extern "C" */
#endif
#endif
\ No newline at end of file
sw/airborne/math/pprz_algebra_float.c
View file @
c6163b37
...
...
@@ -189,12 +189,65 @@ void float_rmat_of_axis_angle(struct FloatRMat *rm, struct FloatVect3 *uv, float
RMAT_ELMT
(
*
rm
,
2
,
2
)
=
uz2
+
(
1
.
-
uz2
)
*
can
;
}
/*@
lemma cos_add:
\forall real a, b;
\cos(a + b) == \cos(a) * \cos(b) - \sin(a)* \sin(b);
*/
/*@
lemma cos_sub:
\forall real a, b;
\cos(a - b) == \cos(a) * \cos(b) + \sin(a)* \sin(b);
*/
/*@
lemma sin_add:
\forall real a, b;
\sin(a + b) == \sin(a) * \cos(b) + \cos(a) * \sin(b);
*/
/*@
lemma sin_sub:
\forall real a, b;
\sin(a - b) == \sin(a) * \cos(b) - \cos(a)* \sin(b);
*/
/*@
lemma cos_sin_square:
\forall real a;
SQR(\cos(a)) + SQR(\sin(a)) == 1.0;
*/
/*@
lemma remarkable_identity_1:
\forall real a, b;
SQR(a + b) == SQR(a) + 2 * a * b + SQR(b);
lemma remarkable_identity_2:
\forall real a, b;
SQR(a - b) == SQR(a) - 2 * a * b + SQR(b);
lemma factorisation:
\forall real a, b, c;
a * b + a * c == a * (b + c);
*/
/*@
lemma float_rmat_of_eulers_321:
\forall real a, b, c;
SQR(\sin(a)) * SQR(\cos(b))
+ SQR(\sin(a) * \sin(b) * \cos(c) - \sin(c) * \cos(a))
+ SQR(\cos(c) * \cos(a) + \sin(a) * \sin(b) * \sin(c)) == 1.0;
*/
/* C n->b rotation matrix */
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
);
...
...
@@ -617,6 +670,18 @@ void float_quat_of_rmat(struct FloatQuat *q, struct FloatRMat *rm)
q
->
qx
=
(
RMAT_ELMT
(
*
rm
,
1
,
2
)
-
RMAT_ELMT
(
*
rm
,
2
,
1
))
/
four_qi
;
q
->
qy
=
(
RMAT_ELMT
(
*
rm
,
2
,
0
)
-
RMAT_ELMT
(
*
rm
,
0
,
2
))
/
four_qi
;
q
->
qz
=
(
RMAT_ELMT
(
*
rm
,
0
,
1
)
-
RMAT_ELMT
(
*
rm
,
1
,
0
))
/
four_qi
;
//@ assert q->qi * q->qi == 0.5* 0.5 * (1 + tr);
//@ assert \at(rm->m[0], Pre) == rm->m[0];
//@ assert \at(rm->m[1], Pre) == rm->m[1];
//@ assert \at(rm->m[2], Pre) == rm->m[2];
//@ assert \at(rm->m[3], Pre) == rm->m[3];
//@ assert \at(rm->m[4], Pre) == rm->m[4];
//@ assert \at(rm->m[5], Pre) == rm->m[5];
//@ assert \at(rm->m[6], Pre) == rm->m[6];
//@ assert \at(rm->m[7], Pre) == rm->m[7];
//@ assert \at(rm->m[8], Pre) == rm->m[8];
//@ assert SQR(rm->m[0]) + SQR(rm->m[1]) + SQR(rm->m[2]) == 1;
//@ assert unary_quaterion(q);
/*printf("tr > 0\n");*/
}
else
{
if
(
RMAT_ELMT
(
*
rm
,
0
,
0
)
>
RMAT_ELMT
(
*
rm
,
1
,
1
)
&&
...
...
sw/airborne/math/pprz_algebra_float.h
View file @
c6163b37
...
...
@@ -586,6 +586,7 @@ extern void float_rmat_of_axis_angle(struct FloatRMat *rm, struct FloatVect3 *uv
/*@
requires valid_FloatRMat(rm);
requires rvalid_FloatEulers(e);
ensures rotation_matrix(l_RMat_of_FloatRMat(rm));
assigns *rm;
*/
extern
void
float_rmat_of_eulers_321
(
struct
FloatRMat
*
rm
,
struct
FloatEulers
*
e
);
...
...
@@ -883,6 +884,7 @@ extern void float_quat_of_orientation_vect(struct FloatQuat *q, const struct Flo
requires rvalid_FloatRMat(rm);
requires rotation_matrix(l_RMat_of_FloatRMat(rm));
requires \separated(rm, q);
ensures unary_quaterion(q);
assigns *q;
behavior trace_pos:
...
...
sw/airborne/math/pprz_algebra_float_convert_rmat_frama_c.h
View file @
c6163b37
...
...
@@ -16,7 +16,7 @@ extern "C" {
* RealRMat definition
* *****************************/
#define SQR(a) (
a*
a)
#define SQR(a) (
(a)*(
a)
)
/*@ ghost
struct RealRMat_s {float a00; float a01; float a02;
...
...
@@ -199,8 +199,6 @@ logic RealRMat l_RMat_of_FloatQuat_bis_2(struct FloatQuat *q) =
* RealQuat definition
* *****************************/
#define SQR(a) (a*a)
/*@ ghost
struct RealQuat_s {float qi;
float qx;
...
...
sw/airborne/math/pprz_algebra_float_frama_c.h
View file @
c6163b37
...
...
@@ -5,6 +5,8 @@
extern
"C"
{
#endif
#include "libc_frama_c.h"
/*******************************
* INTERVAL
* *****************************/
...
...
sw/airborne/math/pprz_algebra_int_frama_c.h
View file @
c6163b37
#ifndef PPRZ_ALGEBRA_INT_FRAM_C_H
#define PPRZ_ALGEBRA_INT_FRAM_C_H
#ifndef PPRZ_ALGEBRA_INT_FRAM
A
_C_H
#define PPRZ_ALGEBRA_INT_FRAM
A
_C_H
#ifdef __cplusplus
extern
"C"
{
...
...
@@ -7,6 +7,8 @@ extern "C" {
#include <limits.h>
#include "libc_frama_c.h"
#define SQRT_INT_MAX 46340
// 46340 = sqrt(INT_MAX);
...
...
@@ -259,39 +261,6 @@ extern "C" {
&& valid_size(c);
*/
/*******************************
* LIBC
* *****************************/
#define PI2 1.5707963
/*@ requires finite_args: \is_finite(x) && \is_finite(y);
requires finite_logic_result: \is_finite(atan2f(x, y));
assigns \result \from x, y;
ensures finite_result: \is_finite(\result);
ensures -PI2 <= \result <= PI2;
*/
extern
float
atan2f
(
float
y
,
float
x
);
/*@ requires in_domain: \is_finite(x) && \abs(x) <= 1;
assigns \result \from x;
ensures finite_result: \is_finite(\result);
ensures -PI2 <= \result <= PI2;
*/
extern
float
asinf
(
float
x
);
/*
typedef struct __fc_lldiv_t {
long long int quot; / Quotient. /
long long int rem; / Remainder. /
} lldiv_t;
*/
/*@ assigns \result \from numer, denom;
ensures \result.quot == numer / denom;
ensures \result.rem == numer % denom; */
extern
lldiv_t
lldiv
(
long
long
int
numer
,
long
long
int
denom
);
/*******************************
* LEMMA for MAT_MUL
* *****************************/
...
...
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