Use default solver in CBMC proof for aws_cryptosdk_keyring_trace_copy…

…_all (aws#677) * Restore YAML file for `aws_cryptosdk_keyring_trace_copy_all` proof * Unset external SAT solver for aws_cryptosdk_keyring_trace_copy_all proof
robin-aws · May 4, 2021 · fa253fc · fa253fc
1 parent 6811e38
commit fa253fc
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 0 deletions.
diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/Makefile
@@ -33,6 +33,11 @@ CBMCFLAGS +=
 DEFINES += -DAWS_NO_STATIC_IMPL
 DEFINES += -DNUM_ELEMS=$(NUM_ELEMS)
 
+# Running this proof with kissat causes it to fail due to kissat
+# getting an "out of memory" error - even if only this proof is running
+# It does not happen with the default solver, so we unset the variable here
+EXTERNAL_SAT_SOLVER =
+
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/array_list.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c

diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/cbmc-batch.yaml
@@ -0,0 +1,4 @@
+:
+  This file marks this directory as containing a CBMC proof. This file
+  is automatically clobbered in CI and replaced with parameters for
+  running the proof.