@@ -89,14 +89,14 @@ void mlk_debug_check_bounds(const char *file, int line, const int16_t *ptr,
8989
9090/* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
9191 * 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), \
9595 (value_lb), (value_ub))))
9696
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), \
100100 (value_abs_bd))))
101101
102102#else /* !MLKEM_DEBUG && CBMC */
0 commit comments