@@ -89,14 +89,14 @@ void mlk_debug_check_bounds(const char *file, int line, const int16_t *ptr,
89
89
90
90
/* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
91
91
* just use a single flattened array_bound(...) here. */
92
- #define mlk_assert_bound_2d (ptr , M , N , value_lb , value_ub ) \
93
- cassert(forall(kN, 0, (M), \
94
- array_bound(&((int16_t (*)[(N)])(ptr))[kN][0], 0, (N), \
92
+ #define mlk_assert_bound_2d (ptr , M , N , value_lb , value_ub ) \
93
+ cassert(forall(kN, 0, (M), \
94
+ array_bound(&((int16_t(*)[(N)])(ptr))[kN][0], 0, (N), \
95
95
(value_lb), (value_ub))))
96
96
97
- #define mlk_assert_abs_bound_2d (ptr , M , N , value_abs_bd ) \
98
- cassert(forall(kN, 0, (M), \
99
- array_abs_bound(&((int16_t (*)[(N)])(ptr))[kN][0], 0, (N), \
97
+ #define mlk_assert_abs_bound_2d (ptr , M , N , value_abs_bd ) \
98
+ cassert(forall(kN, 0, (M), \
99
+ array_abs_bound(&((int16_t(*)[(N)])(ptr))[kN][0], 0, (N), \
100
100
(value_abs_bd))))
101
101
102
102
#else /* !MLKEM_DEBUG && CBMC */
0 commit comments