Skip to content

Commit 48dcccd

Browse files
committed
Fix timeout problem
Signed-off-by: h2parson <[email protected]>
1 parent 926df94 commit 48dcccd

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

cbmc.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -138,7 +138,7 @@
138138
#define array_abs_bound(arr, lb, ub, k) \
139139
array_bound((arr), (lb), (ub), -((int)(k)) + 1, (k))
140140

141-
#define VALID_SLH_VAR_T(var)
141+
#define VALID_SLH_VAR_T(var) \
142142
(memory_no_alias(var, sizeof(slh_var_t)) && memory_no_alias(var->prm, sizeof(slh_param_t)) && \
143143
memory_no_alias(var->adrs, sizeof(adrs_t)))
144144

proofs/cbmc/adrs_set_hash_address/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ REMOVE_FUNCTION_BODY +=
1515
UNWINDSET +=
1616

1717
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
18-
PROJECT_SOURCES += adrs_set_hash_address_harness.c
18+
PROJECT_SOURCES += $(SRCDIR)/slh_sha2.c
1919

2020
CHECK_FUNCTION_CONTRACTS=adrs_set_hash_address
2121
USE_FUNCTION_CONTRACTS=

0 commit comments

Comments
 (0)