chore: update aws-c-common dependency for CBMC proofs

CBMC proofs should use the same version of aws-c-common that customers
will use in their deployments. Stubs that had since been removed from
aws-c-common have now been moved into this repository.

verification/cbmc/include/make_common_data_structures.h

@@ -21,7 +21,6 @@
 #include <aws/cryptosdk/private/header.h>
 #include <aws/cryptosdk/private/hkdf.h>
 #include <proof_helpers/make_common_data_structures.h>
-#include <proof_helpers/proof_allocators.h>
 #include <proof_helpers/utils.h>
 #include <stdint.h>
 #include <stdlib.h>

verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/Makefile

@@ -26,6 +26,7 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 
 CBMCFLAGS +=
 
+PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
@@ -38,7 +39,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.c
 PROJECT_SOURCES += $(SRCDIR)/source/hkdf.c
 
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcpy_override_havoc.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/Makefile

@@ -26,6 +26,7 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 
 CBMCFLAGS +=
 
+PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
@@ -38,7 +39,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.c
 PROJECT_SOURCES += $(SRCDIR)/source/hkdf.c
 
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcpy_override_havoc.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/Makefile

@@ -37,7 +37,6 @@ PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/math.c
 PROJECT_SOURCES += $(SRCDIR)/source/materials.c
 
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/aws_cryptosdk_cmm_base_init_harness.c

@@ -19,7 +19,6 @@
 #include <aws/cryptosdk/materials.h>
 #include <make_common_data_structures.h>
 #include <proof_helpers/make_common_data_structures.h>
-#include <proof_helpers/proof_allocators.h>
 #include <proof_helpers/utils.h>
 
 void aws_cryptosdk_cmm_base_init_harness() {

verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/Makefile

@@ -52,8 +52,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/edk.c
 PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c
 PROJECT_SOURCES += $(SRCDIR)/source/materials.c
 
+PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_table_no_slots_override.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c

verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/aws_cryptosdk_cmm_decrypt_materials_harness.c

@@ -23,7 +23,6 @@
 #include <make_common_data_structures.h>
 #include <proof_helpers/cryptosdk/make_common_data_structures.h>
 #include <proof_helpers/make_common_data_structures.h>
-#include <proof_helpers/proof_allocators.h>
 #include <proof_helpers/utils.h>
 
 // Stub this until https://github.com/diffblue/cbmc/issues/5344 is fixed
@@ -52,7 +51,7 @@ int decrypt_materials(
     assert(AWS_OBJECT_PTR_IS_WRITABLE(output));
     assert(aws_cryptosdk_dec_request_is_valid(request));
 
-    struct aws_cryptosdk_dec_materials *materials = can_fail_malloc(sizeof(*materials));
+    struct aws_cryptosdk_dec_materials *materials = malloc(sizeof(*materials));
     if (materials == NULL) {
         *output = NULL;
         return AWS_OP_ERR;
@@ -92,15 +91,15 @@ void aws_cryptosdk_cmm_decrypt_materials_harness() {
                                                  .decrypt_materials      = nondet_bool() ? decrypt_materials : NULL };
     __CPROVER_assume(aws_cryptosdk_cmm_vtable_is_valid(&vtable));
 
-    struct aws_cryptosdk_cmm *cmm = can_fail_malloc(sizeof(*cmm));
+    struct aws_cryptosdk_cmm *cmm = malloc(sizeof(*cmm));
     __CPROVER_assume(cmm);
     cmm->vtable = &vtable;
     __CPROVER_assume(aws_cryptosdk_cmm_base_is_valid(cmm));
 
-    struct aws_cryptosdk_dec_request *request = can_fail_malloc(sizeof(*request));
+    struct aws_cryptosdk_dec_request *request = malloc(sizeof(*request));
     __CPROVER_assume(request);
-    request->alloc   = can_fail_allocator();
-    request->enc_ctx = can_fail_malloc(sizeof(*request->enc_ctx));
+    request->alloc   = aws_default_allocator();
+    request->enc_ctx = malloc(sizeof(*request->enc_ctx));
     __CPROVER_assume(request->enc_ctx);
     ensure_allocated_hash_table(request->enc_ctx, MAX_NUM_ITEMS);
 
@@ -120,7 +119,7 @@ void aws_cryptosdk_cmm_decrypt_materials_harness() {
     */
     __CPROVER_assume(aws_cryptosdk_dec_request_is_valid(request));
 
-    struct aws_cryptosdk_dec_materials **output = can_fail_malloc(sizeof(*output));
+    struct aws_cryptosdk_dec_materials **output = malloc(sizeof(*output));
     __CPROVER_assume(output);
 
     // Run the function under test.

verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/Makefile

@@ -51,8 +51,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/edk.c
 PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c
 PROJECT_SOURCES += $(SRCDIR)/source/materials.c
 
+PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_table_no_slots_override.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c

verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/aws_cryptosdk_cmm_generate_enc_materials_harness.c

@@ -23,7 +23,6 @@
 #include <make_common_data_structures.h>
 #include <proof_helpers/cryptosdk/make_common_data_structures.h>
 #include <proof_helpers/make_common_data_structures.h>
-#include <proof_helpers/proof_allocators.h>
 #include <proof_helpers/utils.h>
 
 // Stub this until https://github.com/diffblue/cbmc/issues/5344 is fixed
@@ -52,7 +51,7 @@ int generate_enc_materials(
     assert(AWS_OBJECT_PTR_IS_WRITABLE(output));
     assert(aws_cryptosdk_enc_request_is_valid(request));
 
-    struct aws_cryptosdk_enc_materials *materials = can_fail_malloc(sizeof(*materials));
+    struct aws_cryptosdk_enc_materials *materials = malloc(sizeof(*materials));
     if (materials == NULL) {
         *output = NULL;
         return AWS_OP_ERR;
@@ -107,20 +106,20 @@ void aws_cryptosdk_cmm_generate_enc_materials_harness() {
                                                  .decrypt_materials = nondet_voidp() };
     __CPROVER_assume(aws_cryptosdk_cmm_vtable_is_valid(&vtable));
 
-    struct aws_cryptosdk_cmm *cmm = can_fail_malloc(sizeof(*cmm));
+    struct aws_cryptosdk_cmm *cmm = malloc(sizeof(*cmm));
     __CPROVER_assume(cmm);
     cmm->vtable = &vtable;
     __CPROVER_assume(aws_cryptosdk_cmm_base_is_valid(cmm));
 
-    struct aws_cryptosdk_enc_request *request = can_fail_malloc(sizeof(*request));
+    struct aws_cryptosdk_enc_request *request = malloc(sizeof(*request));
     __CPROVER_assume(request);
-    request->alloc   = can_fail_allocator();
-    request->enc_ctx = can_fail_malloc(sizeof(*request->enc_ctx));
+    request->alloc   = aws_default_allocator();
+    request->enc_ctx = malloc(sizeof(*request->enc_ctx));
     __CPROVER_assume(request->enc_ctx);
     ensure_allocated_hash_table(request->enc_ctx, MAX_NUM_ITEMS);
     __CPROVER_assume(aws_cryptosdk_enc_request_is_valid(request));
 
-    struct aws_cryptosdk_enc_materials **output = can_fail_malloc(sizeof(*output));
+    struct aws_cryptosdk_enc_materials **output = malloc(sizeof(*output));
     __CPROVER_assume(output);
 
     // Run the function under test.

verification/cbmc/proofs/aws_cryptosdk_cmm_release/Makefile

@@ -36,7 +36,6 @@ PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/atomics.c
 PROJECT_SOURCES += $(SRCDIR)/source/materials.c
 
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

verification/cbmc/proofs/aws_cryptosdk_cmm_release/aws_cryptosdk_cmm_release_harness.c

@@ -19,7 +19,6 @@
 #include <aws/cryptosdk/materials.h>
 #include <proof_helpers/cryptosdk/make_common_data_structures.h>
 #include <proof_helpers/make_common_data_structures.h>
-#include <proof_helpers/proof_allocators.h>
 #include <proof_helpers/utils.h>
 
 void destroy(struct aws_cryptosdk_cmm *cmm) {
@@ -36,7 +35,7 @@ void aws_cryptosdk_cmm_release_harness() {
                                                  .decrypt_materials      = nondet_voidp() };
     __CPROVER_assume(aws_cryptosdk_cmm_vtable_is_valid(&vtable));
 
-    struct aws_cryptosdk_cmm *cmm = can_fail_malloc(sizeof(struct aws_cryptosdk_cmm));
+    struct aws_cryptosdk_cmm *cmm = malloc(sizeof(struct aws_cryptosdk_cmm));
 
     if (cmm) {
         cmm->vtable = &vtable;

verification/cbmc/proofs/aws_cryptosdk_cmm_retain/Makefile

@@ -38,7 +38,6 @@ PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/atomics.c
 PROJECT_SOURCES += $(SRCDIR)/source/materials.c
 
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

verification/cbmc/proofs/aws_cryptosdk_cmm_retain/aws_cryptosdk_cmm_retain_harness.c

@@ -19,7 +19,6 @@
 #include <aws/cryptosdk/materials.h>
 #include <proof_helpers/cryptosdk/make_common_data_structures.h>
 #include <proof_helpers/make_common_data_structures.h>
-#include <proof_helpers/proof_allocators.h>
 #include <proof_helpers/utils.h>
 
 void aws_cryptosdk_cmm_retain_harness() {

verification/cbmc/proofs/aws_cryptosdk_compare_hash_elems_by_key_string/Makefile

@@ -20,13 +20,13 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 
 CBMCFLAGS +=
 
+PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/string.c
 PROJECT_SOURCES += $(SRCDIR)/source/utils.c
 
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c

verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/Makefile

@@ -52,8 +52,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/edk.c
 PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c
 PROJECT_SOURCES += $(SRCDIR)/source/materials.c
 
+PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_table_no_slots_override.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c

verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/aws_cryptosdk_dec_materials_destroy_harness.c

@@ -23,13 +23,12 @@
 #include <make_common_data_structures.h>
 #include <proof_helpers/cryptosdk/make_common_data_structures.h>
 #include <proof_helpers/make_common_data_structures.h>
-#include <proof_helpers/proof_allocators.h>
 #include <proof_helpers/utils.h>
 
 void aws_cryptosdk_dec_materials_destroy_harness() {
-    struct aws_cryptosdk_dec_materials *materials = can_fail_malloc(sizeof(*materials));
+    struct aws_cryptosdk_dec_materials *materials = malloc(sizeof(*materials));
     if (materials) {
-        materials->alloc = can_fail_allocator();
+        materials->alloc = aws_default_allocator();
         __CPROVER_assume(aws_allocator_is_valid(materials->alloc));
 
         // Set up the signctx

verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/Makefile

@@ -48,8 +48,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/edk.c
 PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c
 PROJECT_SOURCES += $(SRCDIR)/source/materials.c
 
+PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_table_no_slots_override.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c

verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/aws_cryptosdk_dec_materials_new_harness.c

@@ -20,11 +20,10 @@
 #include <cipher_openssl.h>
 #include <proof_helpers/cryptosdk/make_common_data_structures.h>
 #include <proof_helpers/make_common_data_structures.h>
-#include <proof_helpers/proof_allocators.h>
 #include <proof_helpers/utils.h>
 
 void aws_cryptosdk_dec_materials_new_harness() {
-    struct aws_allocator *alloc = can_fail_allocator();
+    struct aws_allocator *alloc = aws_default_allocator();
     enum aws_cryptosdk_alg_id alg;
 
     struct aws_cryptosdk_dec_materials *rval = aws_cryptosdk_dec_materials_new(alloc, alg);

verification/cbmc/proofs/aws_cryptosdk_decrypt_body/Makefile

@@ -34,23 +34,23 @@ CBMCFLAGS +=
 
 DEFINES += -DMAX_BUFFER_SIZE=$(MAX_BUFFER_SIZE)
 
+PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
-PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
 PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/err_override.c
 PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/evp_override.c
 PROJECT_SOURCES += $(SRCDIR)/source/cipher.c
 
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
+PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
+PROOF_SOURCES += $(COMMON_PROOF_UNINLINE)/error.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c
 
 REMOVE_FUNCTION_BODY += EVP_EncryptUpdate
 REMOVE_FUNCTION_BODY += EVP_sha256
 REMOVE_FUNCTION_BODY += EVP_sha384
-REMOVE_FUNCTION_BODY += aws_raise_error_private
 REMOVE_FUNCTION_BODY += nondet_compare
 
 UNWINDSET += aws_cryptosdk_decrypt_body.0:$(call addone,$(MAX_BUFFER_SIZE))

verification/cbmc/proofs/aws_cryptosdk_decrypt_body/aws_cryptosdk_decrypt_body_harness.c

@@ -22,33 +22,33 @@ void aws_cryptosdk_decrypt_body_harness() {
     struct aws_cryptosdk_alg_properties *props = aws_cryptosdk_alg_props(alg_id);
     __CPROVER_assume(aws_cryptosdk_alg_properties_is_valid(props));
 
-    struct aws_byte_buf *outp = can_fail_malloc(sizeof(*outp));
+    struct aws_byte_buf *outp = malloc(sizeof(*outp));
     __CPROVER_assume(outp != NULL);
     __CPROVER_assume(aws_byte_buf_is_bounded(outp, MAX_BUFFER_SIZE));
     ensure_byte_buf_has_allocated_buffer_member(outp);
     __CPROVER_assume(aws_byte_buf_is_valid(outp));
 
-    struct aws_byte_cursor *inp = can_fail_malloc(sizeof(*inp));
+    struct aws_byte_cursor *inp = malloc(sizeof(*inp));
     __CPROVER_assume(inp != NULL);
     __CPROVER_assume(aws_byte_cursor_is_bounded(inp, MAX_BUFFER_SIZE));
     ensure_byte_cursor_has_allocated_buffer_member(inp);
     __CPROVER_assume(aws_byte_cursor_is_valid(inp));
 
-    struct aws_byte_buf *message_id = can_fail_malloc(sizeof(*message_id));
+    struct aws_byte_buf *message_id = malloc(sizeof(*message_id));
     __CPROVER_assume(message_id != NULL);
     __CPROVER_assume(aws_byte_buf_is_bounded(message_id, MAX_BUFFER_SIZE));
     ensure_byte_buf_has_allocated_buffer_member(message_id);
     __CPROVER_assume(aws_byte_buf_is_valid(message_id));
 
     uint32_t seqno;
 
-    uint8_t *iv = can_fail_malloc(props->iv_len);
+    uint8_t *iv = malloc(props->iv_len);
     __CPROVER_assume(iv != NULL);
 
     struct content_key *content_key;
 
     /* Need to allocate tag_len bytes for writing the tag */
-    uint8_t *tag = can_fail_malloc(props->tag_len);
+    uint8_t *tag = malloc(props->tag_len);
     __CPROVER_assume(tag != NULL);
 
     int body_frame_type;

verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/Makefile

@@ -29,10 +29,11 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 CBMCFLAGS +=
 
 PROJECT_SOURCES += $(SRCDIR)/source/default_cmm.c
+PROJECT_SOURCES += $(SRCDIR)/source/header.c
 PROJECT_SOURCES += $(SRCDIR)/source/materials.c
 
+PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/aws_cryptosdk_default_cmm_set_alg_id_harness.c

@@ -35,7 +35,7 @@ void aws_cryptosdk_default_cmm_set_alg_id_harness() {
     __CPROVER_assume(aws_cryptosdk_keyring_is_valid(keyring));
 
     /* Instantiate the default (non-caching) implementation of the Crypto MaterialsManager (CMM) */
-    struct aws_cryptosdk_cmm *cmm = aws_cryptosdk_default_cmm_new(can_fail_allocator(), keyring);
+    struct aws_cryptosdk_cmm *cmm = aws_cryptosdk_default_cmm_new(aws_default_allocator(), keyring);
 
     /* Assumptions */
     __CPROVER_assume(cmm != NULL);

verification/cbmc/proofs/aws_cryptosdk_deserialize_frame/Makefile

@@ -29,7 +29,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c
 PROJECT_SOURCES += $(SRCDIR)/source/framefmt.c
 
 PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
-PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c
 ###########