Remove signctx precondition in harness. Weaken precondition in EVPDig…

…estUpdate
aws · Jan 11, 2021 · 4d0477a · 4d0477a
1 parent c06ea6a
commit 4d0477a
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git a/verification/cbmc/proofs/sign_header/sign_header_harness.c b/verification/cbmc/proofs/sign_header/sign_header_harness.c
@@ -49,7 +49,6 @@ void sign_header_harness() {
         session_setup(MAX_TABLE_SIZE, MAX_TRACE_LIST_ITEMS, MAX_EDK_LIST_ITEMS, MAX_BUFFER_SIZE, MAX_STRING_LEN);
 
     /* Assumptions */
-    __CPROVER_assume(aws_cryptosdk_sig_ctx_is_valid_cbmc(session->signctx));
     __CPROVER_assume(session->alg_props->impl->cipher_ctor != NULL);
     __CPROVER_assume(aws_byte_buf_is_bounded(&session->header.iv, session->alg_props->iv_len));
     __CPROVER_assume(aws_byte_buf_is_bounded(&session->header.auth_tag, session->alg_props->tag_len));

diff --git a/verification/cbmc/sources/openssl/evp_override.c b/verification/cbmc/sources/openssl/evp_override.c
@@ -789,7 +789,7 @@ int EVP_DigestInit(EVP_MD_CTX *ctx, const EVP_MD *type) {
  * on the same ctx to hash additional data. Return values: Returns 1 for success and 0 for failure.
  */
 int EVP_DigestUpdate(EVP_MD_CTX *ctx, const void *d, size_t cnt) {
-    assert(evp_md_ctx_is_valid(ctx));
+    assert(ctx != NULL);
     assert(d);
     assert(AWS_MEM_IS_READABLE(d, cnt));