Skip to content

GitLab

Commit 96c450c0 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Removing is_finite for float and double

parent 7ffcf1a3
Show whitespace changes
Inline Side-by-side
Showing with 120 additions and 323 deletions
README.md
View file @ 96c450c0
......@@ -37,6 +37,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/math/pprz_algebra_double.h
View file @ 96c450c0
......@@ -43,31 +43,12 @@ struct DoubleVect2 {
double y;
};
/*******************************
* DoubleVect3
* *****************************/
struct DoubleVect3 {
double x;
double y;
double z;
};
/*@
predicate finite_DoubleVect3(struct DoubleVect3 *v) =
\is_finite(v->x)
&& \is_finite(v->y)
&& \is_finite(v->z);
*/
/*@
predicate rvalid_DoubleVect3(struct DoubleVect3 *v) =
\valid_read(v) && finite_DoubleVect3(v);
*/
/*******************************
* DoubleQuat
* *****************************/
/**
* @brief Rotation quaternion
*/
......@@ -82,23 +63,6 @@ struct DoubleMat33 {
double m[3 * 3];
};
/*@
predicate finite_DoubleQuat(struct DoubleQuat *q) =
\is_finite(q->qi)
&& \is_finite(q->qx)
&& \is_finite(q->qy)
&& \is_finite(q->qz);
*/
/*@
predicate rvalid_DoubleQuat(struct DoubleQuat *q) =
\valid_read(q) && finite_DoubleQuat(q);
*/
/*******************************
* DoubleRMat
* *****************************/
/**
* @brief rotation matrix
*/
......@@ -106,29 +70,6 @@ struct DoubleRMat {
double m[3 * 3];
};
/*@
predicate finite_DoubleRMat(struct DoubleRMat *rm) =
\is_finite(rm->m[0])
&& \is_finite(rm->m[1])
&& \is_finite(rm->m[2])
&& \is_finite(rm->m[3])
&& \is_finite(rm->m[4])
&& \is_finite(rm->m[5])
&& \is_finite(rm->m[6])
&& \is_finite(rm->m[7])
&& \is_finite(rm->m[8]);
*/
/*@
predicate rvalid_DoubleRMat(struct DoubleRMat *rm) =
\valid_read(rm) && finite_DoubleRMat(rm);
*/
/*******************************
* DoubleEulers
* *****************************/
/**
* @brief euler angles
* @details Units: radians */
......@@ -147,18 +88,6 @@ struct DoubleRates {
double r; ///< in rad/s^2
};
/*@
predicate finite_DoubleEulers(struct DoubleEulers *e) =
\is_finite(e->phi)
&& \is_finite(e->theta)
&& \is_finite(e->psi);
*/
/*@
predicate rvalid_DoubleEulers(struct DoubleEulers *e) =
\valid_read(e) && finite_DoubleEulers(e);
*/
#include "pprz_algebra_double_frama_c.h"
#define DOUBLE_VECT3_ROUND(_v) DOUBLE_VECT3_RINT(_v, _v)
......@@ -247,26 +176,26 @@ static inline void double_quat_normalize(struct DoubleQuat *q)
/*ensures is_rotation_matrix(rm);*/
/*@
requires \valid(rm);
requires rvalid_DoubleEulers(e);
requires \valid_read(e);
assigns *rm;
*/
extern void double_rmat_of_eulers_321(struct DoubleRMat *rm, struct DoubleEulers *e);
/*@
requires \valid(q);
requires rvalid_DoubleEulers(e);
requires \valid_read(e);
assigns *q;
*/
extern void double_quat_of_eulers(struct DoubleQuat *q, struct DoubleEulers *e);
/*@
requires \valid(e);
requires rvalid_DoubleQuat(q);
requires \valid_read(q);
assigns *e;
*/
extern void double_eulers_of_quat(struct DoubleEulers *e, struct DoubleQuat *q);
/*@
requires \valid(v_out);
requires rvalid_DoubleQuat(q);
requires rvalid_DoubleVect3(v_in);
requires \valid_read(q);
requires \valid_read(v_in);
assigns *v_out;
*/
extern void double_quat_vmult(struct DoubleVect3 *v_out, struct DoubleQuat *q, struct DoubleVect3 *v_in);
......@@ -286,7 +215,7 @@ static inline void double_rmat_identity(struct DoubleRMat *rm)
*/
/*@
requires \valid(m_b2a);
requires rvalid_DoubleRMat(m_a2b);
requires \valid_read(m_a2b);
assigns *m_b2a;
*/
extern void double_rmat_inv(struct DoubleRMat *m_b2a, struct DoubleRMat *m_a2b);
......@@ -296,8 +225,8 @@ extern void double_rmat_inv(struct DoubleRMat *m_b2a, struct DoubleRMat *m_a2b);
*/
/*@
requires \valid(m_a2c);
requires rvalid_DoubleRMat(m_a2b);
requires rvalid_DoubleRMat(m_b2c);
requires \valid_read(m_a2b);
requires \valid_read(m_b2c);
assigns *m_a2c;
*/
extern void double_rmat_comp(struct DoubleRMat *m_a2c, struct DoubleRMat *m_a2b,
......@@ -308,8 +237,8 @@ extern void double_rmat_comp(struct DoubleRMat *m_a2c, struct DoubleRMat *m_a2b,
*/
/*@
requires \valid(vb);
requires rvalid_DoubleRMat(m_a2b);
requires rvalid_DoubleVect3(va);
requires \valid_read(m_a2b);
requires \valid_read(va);
assigns *vb;
*/
extern void double_rmat_vmult(struct DoubleVect3 *vb, struct DoubleRMat *m_a2b,
......@@ -320,15 +249,15 @@ extern void double_rmat_vmult(struct DoubleVect3 *vb, struct DoubleRMat *m_a2b,
*/
/*@
requires \valid(vb);
requires rvalid_DoubleRMat(m_b2a);
requires rvalid_DoubleVect3(va);
requires \valid_read(m_b2a);
requires \valid_read(va);
assigns *vb;
*/
extern void double_rmat_transp_vmult(struct DoubleVect3 *vb, struct DoubleRMat *m_b2a,
struct DoubleVect3 *va);
/*@
requires \valid(rm);
requires rvalid_DoubleQuat(q);
requires \valid_read(q);
assigns *rm;
*/
extern void double_rmat_of_quat(struct DoubleRMat *rm, struct DoubleQuat *q);
......
sw/airborne/math/pprz_algebra_float.h
View file @ 96c450c0
......@@ -48,63 +48,17 @@ extern "C" {
#define M_SQRT2 1.41421356237309504880
#endif
/*******************************
* FloatVect2
* *****************************/
struct FloatVect2 {
float x;
float y;
};
/*@
predicate finite_FloatVect2(struct FloatVect2 *v) =
\is_finite(v->x)
&& \is_finite(v->y);
*/
/*@
predicate rvalid_FloatVect2(struct FloatVect2 *v) =
\valid_read(v) && finite_FloatVect2(v);
*/
/*@
predicate valid_FloatVect2(struct FloatVect2 *v) =
\valid(v) && finite_FloatVect2(v);
*/
/*******************************
* FloatVect3
* *****************************/
struct FloatVect3 {
float x;
float y;
float z;
};
/*@
predicate finite_FloatVect3(struct FloatVect3 *v) =
\is_finite(v->x)
&& \is_finite(v->y)
&& \is_finite(v->z);
*/
/*@
predicate rvalid_FloatVect3(struct FloatVect3 *v) =
\valid_read(v) && finite_FloatVect3(v);
*/
/*@
predicate valid_FloatVect3(struct FloatVect3 *v) =
\valid(v) && finite_FloatVect3(v);
*/
/*******************************
* FloatQuat
* *****************************/
/**
* @brief Roation quaternion
*/
......@@ -119,36 +73,6 @@ struct FloatMat33 {
float m[3 * 3];
};
/*@
predicate finite_FloatQuat(struct FloatQuat *q) =
\is_finite(q->qi)
&& \is_finite(q->qx)
&& \is_finite(q->qy)
&& \is_finite(q->qz);
*/
/*@
predicate rvalid_FloatQuat(struct FloatQuat *q) =
\valid_read(q) && finite_FloatQuat(q);
*/
/*@
predicate valid_FloatQuat(struct FloatQuat *q) =
\valid(q) && finite_FloatQuat(q);
*/
/*@
predicate valid_subterms_FloatQuat(struct FloatQuat *q) =
\valid(&q->qi)
&& \valid(&q->qx)
&& \valid(&q->qy)
&& \valid(&q->qz);
*/
/*******************************
* FloatRMat
* *****************************/
/**
* @brief rotation matrix
*/
......@@ -156,35 +80,6 @@ struct FloatRMat {
float m[3 * 3];
};
/*@
predicate finite_FloatRMat(struct FloatRMat *rm) =
\is_finite(rm->m[0])
&& \is_finite(rm->m[1])
&& \is_finite(rm->m[2])
&& \is_finite(rm->m[3])
&& \is_finite(rm->m[4])
&& \is_finite(rm->m[5])
&& \is_finite(rm->m[6])
&& \is_finite(rm->m[7])
&& \is_finite(rm->m[8]);
*/
/*@
predicate rvalid_FloatRMat(struct FloatRMat *rm) =
\valid_read(rm) && finite_FloatRMat(rm);
*/
/*@
predicate valid_FloatRMat(struct FloatRMat *rm) =
\valid(rm) && finite_FloatRMat(rm);
*/
/*******************************
* FloatEulers
* *****************************/
/**
* @brief euler angles
* @details Units: radians */
......@@ -194,23 +89,6 @@ struct FloatEulers {
float psi; ///< in radians
};
/*@
predicate finite_FloatEulers(struct FloatEulers *e) =
\is_finite(e->phi)
&& \is_finite(e->theta)
&& \is_finite(e->psi);
*/
/*@
predicate rvalid_FloatEulers(struct FloatEulers *e) =
\valid_read(e) && finite_FloatEulers(e);
*/
/*@
predicate valid_FloatEulers(struct FloatEulers *e) =
\valid(e) && finite_FloatEulers(e);
*/
/**
* @brief angular rates
* @details Units: rad/s */
......@@ -220,23 +98,6 @@ struct FloatRates {
float r; ///< in rad/s
};
/*@
predicate finite_FloatRates(struct FloatRates *r) =
\is_finite(r->p)
&& \is_finite(r->q)
&& \is_finite(r->r);
*/
/*@
predicate rvalid_FloatRates(struct FloatRates *r) =
\valid_read(r) && finite_FloatRates(r);
*/
/*@
predicate valid_FloatRates(struct FloatRates *r) =
\valid(r) && finite_FloatRates(r);
*/
#define FLOAT_ANGLE_NORMALIZE(_a) { \
while (_a > M_PI) _a -= (2.*M_PI); \
while (_a < -M_PI) _a += (2.*M_PI); \
......@@ -376,23 +237,23 @@ static inline void float_vect3_normalize(struct FloatVect3 *v)
}
/*@
requires valid_FloatVect3(vec);
requires rvalid_FloatVect3(dv);
requires \valid(vec);
requires \valid_read(dv);
assigns *vec;
*/
extern void float_vect3_integrate_fi(struct FloatVect3 *vec, struct FloatVect3 *dv,
float dt);
/*@
requires valid_FloatRates(r);
requires rvalid_FloatRates(dr);
requires \valid(r);
requires \valid_read(dr);
assigns *r;
*/
extern void float_rates_integrate_fi(struct FloatRates *r, struct FloatRates *dr,
float dt);
/*@
requires valid_FloatRates(r);
requires rvalid_FloatEulers(e);
requires rvalid_FloatEulers(edot);
requires \valid(r);
requires \valid_read(e);
requires \valid_read(edot);
assigns *r;
*/
extern void float_rates_of_euler_dot(struct FloatRates *r, struct FloatEulers *e,
......@@ -454,7 +315,7 @@ static inline void float_rmat_identity(struct FloatRMat *rm)
*/
/*@
requires \valid(m_b2a);
requires rvalid_FloatRMat(m_a2b);
requires \valid_read(m_a2b);
assigns *m_b2a;
*/
extern void float_rmat_inv(struct FloatRMat *m_b2a, struct FloatRMat *m_a2b);
......@@ -463,9 +324,9 @@ extern void float_rmat_inv(struct FloatRMat *m_b2a, struct FloatRMat *m_a2b);
* m_a2c = m_a2b comp m_b2c , aka m_a2c = m_b2c * m_a2b
*/
/*@
requires valid_FloatRMat(m_a2c);
requires rvalid_FloatRMat(m_a2b);
requires rvalid_FloatRMat(m_b2c);
requires \valid(m_a2c);
requires \valid_read(m_a2b);
requires \valid_read(m_b2c);
requires \separated(m_a2c + (0..8), m_a2b + (0..8), m_b2c + (0..8));
assigns m_a2c[0..8];
*/
......@@ -476,9 +337,9 @@ extern void float_rmat_comp(struct FloatRMat *m_a2c, struct FloatRMat *m_a2b,
* m_a2b = m_a2c comp_inv m_b2c , aka m_a2b = inv(_m_b2c) * m_a2c
*/
/*@
requires valid_FloatRMat(m_a2b);
requires rvalid_FloatRMat(m_a2c);
requires rvalid_FloatRMat(m_b2c);
requires \valid(m_a2b);
requires \valid_read(m_a2c);
requires \valid_read(m_b2c);
assigns m_a2b[0..8];
*/
extern void float_rmat_comp_inv(struct FloatRMat *m_a2b, struct FloatRMat *m_a2c,
......@@ -486,7 +347,7 @@ extern void float_rmat_comp_inv(struct FloatRMat *m_a2b, struct FloatRMat *m_a2c
/// Norm of a rotation matrix.
/*@
requires rvalid_FloatRMat(rm);
requires \valid_read(rm);
assigns \nothing;
*/
extern float float_rmat_norm(struct FloatRMat *rm);
......@@ -495,9 +356,9 @@ extern float float_rmat_norm(struct FloatRMat *rm);
* vb = m_a2b * va
*/
/*@
requires valid_FloatVect3(vb);
requires rvalid_FloatRMat(m_a2b);
requires rvalid_FloatVect3(va);
requires \valid(vb);
requires \valid_read(m_a2b);
requires \valid_read(va);
assigns *vb;
*/
extern void float_rmat_vmult(struct FloatVect3 *vb, struct FloatRMat *m_a2b,
......@@ -507,9 +368,9 @@ extern void float_rmat_vmult(struct FloatVect3 *vb, struct FloatRMat *m_a2b,
* vb = m_b2a^T * va
*/
/*@
requires valid_FloatVect3(vb);
requires rvalid_FloatRMat(m_b2a);
requires rvalid_FloatVect3(va);
requires \valid(vb);
requires \valid_read(m_b2a);
requires \valid_read(va);
assigns *vb;
*/
extern void float_rmat_transp_vmult(struct FloatVect3 *vb, struct FloatRMat *m_b2a,
......@@ -519,9 +380,9 @@ extern void float_rmat_transp_vmult(struct FloatVect3 *vb, struct FloatRMat *m_b
* rb = m_a2b * ra
*/
/*@
requires valid_FloatEulers(rb);
requires rvalid_FloatRMat(m_a2b);
requires rvalid_FloatEulers(ra);
requires \valid(rb);
requires \valid_read(m_a2b);
requires \valid_read(ra);
assigns *rb;
*/
extern void float_rmat_mult(struct FloatEulers *rb, struct FloatRMat *m_a2b,
......@@ -531,9 +392,9 @@ extern void float_rmat_mult(struct FloatEulers *rb, struct FloatRMat *m_a2b,
* rb = m_b2a^T * ra
*/
/*@
requires valid_FloatEulers(rb);
requires rvalid_FloatRMat(m_b2a);
requires rvalid_FloatEulers(ra);
requires \valid(rb);
requires \valid_read(m_b2a);
requires \valid_read(ra);
assigns *rb;
*/
extern void float_rmat_transp_mult(struct FloatEulers *rb, struct FloatRMat *m_b2a,
......@@ -543,9 +404,9 @@ extern void float_rmat_transp_mult(struct FloatEulers *rb, struct FloatRMat *m_b
* rb = m_a2b * ra
*/
/*@
requires valid_FloatRates(rb);
requires rvalid_FloatRMat(m_a2b);
requires rvalid_FloatRates(ra);
requires \valid(rb);
requires \valid_read(m_a2b);
requires \valid_read(ra);
assigns *rb;
*/
extern void float_rmat_ratemult(struct FloatRates *rb, struct FloatRMat *m_a2b,
......@@ -555,9 +416,9 @@ extern void float_rmat_ratemult(struct FloatRates *rb, struct FloatRMat *m_a2b,
* rb = m_b2a^T * ra
*/
/*@
requires valid_FloatRates(rb);
requires rvalid_FloatRMat(m_b2a);
requires rvalid_FloatRates(ra);
requires \valid(rb);
requires \valid_read(m_b2a);
requires \valid_read(ra);
assigns *rb;
*/
extern void float_rmat_transp_ratemult(struct FloatRates *rb, struct FloatRMat *m_b2a,
......@@ -565,8 +426,8 @@ extern void float_rmat_transp_ratemult(struct FloatRates *rb, struct FloatRMat *
/** initialises a rotation matrix from unit vector axis and angle */
/*@
requires valid_FloatRMat(rm);
requires rvalid_FloatVect3(uv);
requires \valid(rm);
requires \valid_read(uv);
assigns *rm;
*/
extern void float_rmat_of_axis_angle(struct FloatRMat *rm, struct FloatVect3 *uv, float angle);
......@@ -584,16 +445,16 @@ extern void float_rmat_of_axis_angle(struct FloatRMat *rm, struct FloatVect3 *uv
* @param[in] e pointer to Euler angles
*/
/*@
requires valid_FloatRMat(rm);
requires rvalid_FloatEulers(e);
requires \valid(rm);
requires \valid_read(e);
ensures rotation_matrix(l_RMat_of_FloatRMat(rm));
ensures special_orthogonal(l_RMat_of_FloatRMat(rm));
assigns *rm;
*/
extern void float_rmat_of_eulers_321(struct FloatRMat *rm, struct FloatEulers *e);
/*@
requires valid_FloatRMat(rm);
requires rvalid_FloatEulers(e);
requires \valid(rm);
requires \valid_read(e);
ensures rotation_matrix(l_RMat_of_FloatRMat(rm));
ensures special_orthogonal(l_RMat_of_FloatRMat(rm));
assigns *rm;
......@@ -602,8 +463,8 @@ extern void float_rmat_of_eulers_312(struct FloatRMat *rm, struct FloatEulers *e
#define float_rmat_of_eulers float_rmat_of_eulers_321
/*@
requires valid_FloatRMat(rm);
requires rvalid_FloatQuat(q);
requires \valid(rm);
requires \valid_read(q);
requires unary_quaternion(q);
requires \separated(rm, q);
ensures transpose(l_RMat_of_FloatRMat(rm)) == l_RMat_of_FloatQuat(q);
......@@ -615,13 +476,13 @@ extern void float_rmat_of_quat(struct FloatRMat *rm, struct FloatQuat *q);
/** in place first order integration of a rotation matrix */
/*@
requires valid_FloatRMat(rm);
requires rvalid_FloatRates(omega);
requires \valid(rm);
requires \valid_read(omega);
assigns *rm;
*/
extern void float_rmat_integrate_fi(struct FloatRMat *rm, struct FloatRates *omega, float dt);
/*@
requires valid_FloatRMat(rm);
requires \valid(rm);
assigns *rm;
*/
extern float float_rmat_reorthogonalize(struct FloatRMat *rm);
......@@ -717,9 +578,9 @@ static inline void float_quat_wrap_shortest(struct FloatQuat *q)
* a2c = a2b comp b2c , aka a2c = a2b * b2c
*/
/*@
requires valid_FloatQuat(a2c);
requires rvalid_FloatQuat(a2b);
requires rvalid_FloatQuat(b2c);
requires \valid(a2c);
requires \valid_read(a2b);
requires \valid_read(b2c);
assigns *a2c;
*/
extern void float_quat_comp(struct FloatQuat *a2c, struct FloatQuat *a2b, struct FloatQuat *b2c);
......@@ -728,9 +589,9 @@ extern void float_quat_comp(struct FloatQuat *a2c, struct FloatQuat *a2b, struct
* a2b = a2c comp_inv b2c , aka a2b = a2c * inv(b2c)
*/
/*@
requires valid_FloatQuat(a2b);
requires rvalid_FloatQuat(a2c);
requires rvalid_FloatQuat(b2c);
requires \valid(a2b);
requires \valid_read(a2c);
requires \valid_read(b2c);
assigns *a2b;
*/
extern void float_quat_comp_inv(struct FloatQuat *a2b, struct FloatQuat *a2c, struct FloatQuat *b2c);
......@@ -739,9 +600,9 @@ extern void float_quat_comp_inv(struct FloatQuat *a2b, struct FloatQuat *a2c, st
* b2c = a2b inv_comp a2c , aka b2c = inv(_a2b) * a2c
*/
/*@
requires valid_FloatQuat(b2c);
requires rvalid_FloatQuat(a2b);
requires rvalid_FloatQuat(a2c);
requires \valid(b2c);
requires \valid_read(a2b);
requires \valid_read(a2c);
assigns *b2c;
*/
extern void float_quat_inv_comp(struct FloatQuat *b2c, struct FloatQuat *a2b, struct FloatQuat *a2c);
......@@ -750,9 +611,9 @@ extern void float_quat_inv_comp(struct FloatQuat *b2c, struct FloatQuat *a2b, st
* a2c = a2b comp b2c , aka a2c = a2b * b2c
*/
/*@
requires valid_FloatQuat(a2c);
requires rvalid_FloatQuat(a2b);
requires rvalid_FloatQuat(b2c);
requires \valid(a2c);
requires \valid_read(a2b);
requires \valid_read(b2c);
assigns *a2c;
*/
extern void float_quat_comp_norm_shortest(struct FloatQuat *a2c, struct FloatQuat *a2b, struct FloatQuat *b2c);
......@@ -761,9 +622,9 @@ extern void float_quat_comp_norm_shortest(struct FloatQuat *a2c, struct FloatQua
* a2b = a2c comp_inv b2c , aka a2b = a2c * inv(b2c)
*/
/*@
requires valid_FloatQuat(a2b);
requires rvalid_FloatQuat(a2c);
requires rvalid_FloatQuat(b2c);
requires \valid(a2b);<