unbounded

microsoft · Jul 29, 2024 · fac7905 · fac7905
1 parent cbfc288
commit fac7905
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/CBMC/proofs/SymCryptAesEcb/Makefile b/CBMC/proofs/SymCryptAesEcb/Makefile
@@ -41,7 +41,8 @@ CBMC_FLAG_SIGNED_OVERFLOW_CHECK ?=
 CBMC_FLAG_UNDEFINED_SHIFT_CHECK ?=
 CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK =
 CBMC_FLAG_UNWINDING_ASSERTIONS ?= --unwinding-assertions
-CBMC_DEFAULT_UNWIND ?= --unwind 10
+CBMC_DEFAULT_UNWIND ?= --unwind 25
+CBMC_OBJECT_BITS ?= 9
 # If you require access to a file-local ("static") function or object to conduct
 # your proof, set the following (and do not include the original source file
 # ("lib/aes-c.c") in PROJECT_SOURCES).

diff --git a/CBMC/proofs/SymCryptAesEcb/SymCryptAesEcb_harness.c b/CBMC/proofs/SymCryptAesEcb/SymCryptAesEcb_harness.c
@@ -35,6 +35,7 @@ void harness(void)
     __CPROVER_assume(pbKey != NULL);
     PSYMCRYPT_AES_EXPANDED_KEY pExpandedKey;
     pExpandedKey = malloc(SYMCRYPT_AES_EXPANDED_KEY_SIZE);
+    __CPROVER_assume(pExpandedKey != NULL);
     SymCryptAesExpandKey( pExpandedKey, pbKey, cbKey );
     free(pbKey);
     free(pExpandedKey);