Skip to content

Commit 216176f

Browse files
committed
CBMC: Increase OBJECT_BITS for various proofs
CBMC: polyvec_matrix-expand OBJECT_BITS 10 -> 11 CBMC: polyvecl_pointwise_acc_montgomery OBJECT_BITS 10->12 CBMC: polyvecl_chknorm OBJECT_BITS 9->12 Signed-off-by: Matthias J. Kannwischer <[email protected]>
1 parent a61b5e0 commit 216176f

File tree

3 files changed

+3
-3
lines changed

3 files changed

+3
-3
lines changed

proofs/cbmc/polyvec_matrix_expand/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ FUNCTION_NAME = polyvec_matrix_expand
3737
# EXPENSIVE = true
3838

3939
# This function is large enough to need...
40-
CBMC_OBJECT_BITS = 10
40+
CBMC_OBJECT_BITS = 11
4141

4242
# If you require access to a file-local ("static") function or object to conduct
4343
# your proof, set the following (and do not include the original source file

proofs/cbmc/polyvecl_chknorm/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ FUNCTION_NAME = polyvecl_chknorm
3939
# EXPENSIVE = true
4040

4141
# This function is large enough to need...
42-
CBMC_OBJECT_BITS = 9
42+
CBMC_OBJECT_BITS = 12
4343

4444
# If you require access to a file-local ("static") function or object to conduct
4545
# your proof, set the following (and do not include the original source file

proofs/cbmc/polyvecl_pointwise_acc_montgomery/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ FUNCTION_NAME = polyvecl_pointwise_acc_montgomery
3737
# EXPENSIVE = true
3838

3939
# This function is large enough to need...
40-
CBMC_OBJECT_BITS = 10
40+
CBMC_OBJECT_BITS = 12
4141

4242
# If you require access to a file-local ("static") function or object to conduct
4343
# your proof, set the following (and do not include the original source file

0 commit comments

Comments
 (0)