Skip to content

Commit 9c8f5b9

Browse files
committed
CBMC: Fix documentation of array_abs_bound
Signed-off-by: Matthias J. Kannwischer <[email protected]>
1 parent f8ae3ea commit 9c8f5b9

File tree

1 file changed

+4
-2
lines changed

1 file changed

+4
-2
lines changed

mldsa/cbmc.h

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -119,8 +119,10 @@
119119

120120
/* Wrapper around array_bound operating on absolute values.
121121
*
122-
* Note that since the absolute bound is inclusive, but the lower
123-
* bound in array_bound is inclusive, we have to raise it by 1.
122+
* The absolute value bound `k` is exclusive.
123+
*
124+
* Note that since the lower bound in array_bound is inclusive, we have to
125+
* raise it by 1 here.
124126
*/
125127
#define array_abs_bound(arr, lb, ub, k) \
126128
array_bound((arr), (lb), (ub), -((int)(k)) + 1, (k))

0 commit comments

Comments
 (0)