Commit 589e07c1 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Removing all unecessary assert

parent a5543c38
......@@ -197,6 +197,6 @@ tests/results/*
# Frama-C
**/.frama-c
!sw/airborne/.frama-c
!sw/airborne/.frama-c/wp/script
**/.lia.cache
**/tmp_wp_analysis.txt
\ No newline at end of file
**/tmp_wp_analysis.txt
This diff is collapsed.
......@@ -4,4 +4,4 @@
"pattern": "P_rvalid_int_mat_3_$Malloc$Mptr[=]" },
"children": { "Unfold 'P_rvalid_int_mat_3_'": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 2.23 } ] } } ]
"time": 2.37 } ] } } ]
......@@ -4,4 +4,4 @@
"target": "let a_0 = (shiftfield_F15_Int32RMat_m r_3) in\n(lsl\n (to_sint32\n (\\truncate\n (16384+\n (real_of_int\n (Mint_24[(shift_sint32 a_0 8)]-Mint_24[(shift_sint32 a_0 0)]-\n Mint_24[(shift_sint32 a_0 4)]))))) 14)",
"pattern": "lslto_sint3214\\truncate+16384real_of_int" },
"children": { "gen_shift": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 0.13 } ] } } ]
"verdict": "valid", "time": 0.15 } ] } } ]
......@@ -4,4 +4,4 @@
"target": "let a_0 = (shiftfield_F15_Int32RMat_m r_1) in\n(lsl\n (to_sint32\n (\\truncate\n (16384+\n (real_of_int\n (Mint_12[(shift_sint32 a_0 0)]-Mint_12[(shift_sint32 a_0 4)]-\n Mint_12[(shift_sint32 a_0 8)]))))) 14)",
"pattern": "lslto_sint3214\\truncate+16384real_of_int" },
"children": { "gen_shift": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 0.15 } ] } } ]
"verdict": "valid", "time": 0.14 } ] } } ]
......@@ -4,5 +4,5 @@
"target": "(lsr (to_sint32 (stheta_0*Mint_3[(shiftfield_F14_Int32Eulers_psi ed_0)])) 14)",
"pattern": "lsrto_sint3214*$stheta[]$Mintshiftfield_F14_Int32Eulers_psi" },
"children": { "gen_shift": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 0.0978,
"verdict": "valid", "time": 0.0563,
"steps": 244 } ] } } ]
......@@ -1387,6 +1387,8 @@ static inline void float_mat_mul(float **o, float **a, float **b, int m, int n,
}
}
/* Ignoring functions that are not supported by frama-c */
#ifndef FRAMA_C_ANALYSIS
/** o = a * b
*
* a: [m x n]
......@@ -1398,23 +1400,23 @@ static inline void float_mat_mul(float **o, float **a, float **b, int m, int n,
* of the input matrices when this function is used, which is useful for consecutive multiplications
* (e.g. when doing matrix exponentiation), at the cost of some copy overhead.
*/
// static inline void float_mat_mul_copy(float **o, float **a, float **b, int m, int n, int l)
// {
// float temp[m][l];
// int i, j, k;
// for (i = 0; i < m; i++) {
// for (j = 0; j < l; j++) {
// temp[i][j] = 0.;
// for (k = 0; k < n; k++) {
// temp[i][j] += a[i][k] * b[k][j];
// }
// }
// }
// MAKE_MATRIX_PTR(_o, o, m);
// MAKE_MATRIX_PTR(_temp, temp, m);
// float_mat_copy(_o, _temp, m, l);
// }
static inline void float_mat_mul_copy(float **o, float **a, float **b, int m, int n, int l)
{
float temp[m][l];
int i, j, k;
for (i = 0; i < m; i++) {
for (j = 0; j < l; j++) {
temp[i][j] = 0.;
for (k = 0; k < n; k++) {
temp[i][j] += a[i][k] * b[k][j];
}
}
}
MAKE_MATRIX_PTR(_o, o, m);
MAKE_MATRIX_PTR(_temp, temp, m);
float_mat_copy(_o, _temp, m, l);
}
#endif
/** o = a * b
*
......
This diff is collapsed.
......@@ -466,7 +466,6 @@ static inline void int32_vect2_normalize(struct Int32Vect2 *v, uint8_t frac)
const uint32_t n = int32_vect2_norm(v);
if (n > 0) {
const int32_t f = BFP_OF_REAL((1.), frac);
//@ assert 0 <= (1 << frac) <= SQRT_INT_MAX;
v->x = v->x * f / (int32_t)n;
v->y = v->y * f / (int32_t)n;
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment