Skip to content

Commit 659d548

Browse files
tautschnigtautschnig
committed
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.
1 parent 6174f83 commit 659d548

File tree

181 files changed

+422
-390
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

181 files changed

+422
-390
lines changed

‎verification/cbmc/aws-c-common

Submodule aws-c-common updated 891 files

‎verification/cbmc/include/make_common_data_structures.h

-1
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@
2020
#include <aws/cryptosdk/private/framefmt.h>
2121
#include <aws/cryptosdk/private/header.h>
2222
#include <proof_helpers/make_common_data_structures.h>
23-
#include <proof_helpers/proof_allocators.h>
2423
#include <proof_helpers/utils.h>
2524
#include <stdint.h>
2625
#include <stdlib.h>

‎verification/cbmc/include/proof_allocators.h

-23
This file was deleted.

‎verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
2626

2727
CBMCFLAGS +=
2828

29+
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
2930
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c
3031
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
3132
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
@@ -38,7 +39,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.c
3839
PROJECT_SOURCES += $(SRCDIR)/source/hkdf.c
3940

4041
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
41-
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
4242
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
4343
PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcpy_override_havoc.c
4444
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

‎verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
2626

2727
CBMCFLAGS +=
2828

29+
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
2930
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c
3031
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
3132
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
@@ -38,7 +39,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.c
3839
PROJECT_SOURCES += $(SRCDIR)/source/hkdf.c
3940

4041
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
41-
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
4242
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
4343
PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcpy_override_havoc.c
4444
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

‎verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,6 @@ PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/math.c
3737
PROJECT_SOURCES += $(SRCDIR)/source/materials.c
3838

3939
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
40-
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
4140
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
4241
PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
4342
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

‎verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/aws_cryptosdk_cmm_base_init_harness.c

-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,6 @@
1919
#include <aws/cryptosdk/materials.h>
2020
#include <make_common_data_structures.h>
2121
#include <proof_helpers/make_common_data_structures.h>
22-
#include <proof_helpers/proof_allocators.h>
2322
#include <proof_helpers/utils.h>
2423

2524
void aws_cryptosdk_cmm_base_init_harness() {

‎verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -52,8 +52,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/edk.c
5252
PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c
5353
PROJECT_SOURCES += $(SRCDIR)/source/materials.c
5454

55+
PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
5556
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
56-
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
5757
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
5858
PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_table_no_slots_override.c
5959
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

+6-7
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,6 @@
2323
#include <make_common_data_structures.h>
2424
#include <proof_helpers/cryptosdk/make_common_data_structures.h>
2525
#include <proof_helpers/make_common_data_structures.h>
26-
#include <proof_helpers/proof_allocators.h>
2726
#include <proof_helpers/utils.h>
2827

2928
// Stub this until https://github.com/diffblue/cbmc/issues/5344 is fixed
@@ -52,7 +51,7 @@ int decrypt_materials(
5251
assert(AWS_OBJECT_PTR_IS_WRITABLE(output));
5352
assert(aws_cryptosdk_dec_request_is_valid(request));
5453

55-
struct aws_cryptosdk_dec_materials *materials = can_fail_malloc(sizeof(*materials));
54+
struct aws_cryptosdk_dec_materials *materials = malloc(sizeof(*materials));
5655
if (materials == NULL) {
5756
*output = NULL;
5857
return AWS_OP_ERR;
@@ -92,15 +91,15 @@ void aws_cryptosdk_cmm_decrypt_materials_harness() {
9291
.decrypt_materials = nondet_bool() ? decrypt_materials : NULL };
9392
__CPROVER_assume(aws_cryptosdk_cmm_vtable_is_valid(&vtable));
9493

95-
struct aws_cryptosdk_cmm *cmm = can_fail_malloc(sizeof(*cmm));
94+
struct aws_cryptosdk_cmm *cmm = malloc(sizeof(*cmm));
9695
__CPROVER_assume(cmm);
9796
cmm->vtable = &vtable;
9897
__CPROVER_assume(aws_cryptosdk_cmm_base_is_valid(cmm));
9998

100-
struct aws_cryptosdk_dec_request *request = can_fail_malloc(sizeof(*request));
99+
struct aws_cryptosdk_dec_request *request = malloc(sizeof(*request));
101100
__CPROVER_assume(request);
102-
request->alloc = can_fail_allocator();
103-
request->enc_ctx = can_fail_malloc(sizeof(*request->enc_ctx));
101+
request->alloc = aws_default_allocator();
102+
request->enc_ctx = malloc(sizeof(*request->enc_ctx));
104103
__CPROVER_assume(request->enc_ctx);
105104
ensure_allocated_hash_table(request->enc_ctx, MAX_NUM_ITEMS);
106105

@@ -120,7 +119,7 @@ void aws_cryptosdk_cmm_decrypt_materials_harness() {
120119
*/
121120
__CPROVER_assume(aws_cryptosdk_dec_request_is_valid(request));
122121

123-
struct aws_cryptosdk_enc_materials **output = can_fail_malloc(sizeof(*output));
122+
struct aws_cryptosdk_dec_materials **output = malloc(sizeof(*output));
124123
__CPROVER_assume(output);
125124

126125
// Run the function under test.

‎verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -51,8 +51,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/edk.c
5151
PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c
5252
PROJECT_SOURCES += $(SRCDIR)/source/materials.c
5353

54+
PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
5455
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
55-
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
5656
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
5757
PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_table_no_slots_override.c
5858
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

+6-7
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,6 @@
2323
#include <make_common_data_structures.h>
2424
#include <proof_helpers/cryptosdk/make_common_data_structures.h>
2525
#include <proof_helpers/make_common_data_structures.h>
26-
#include <proof_helpers/proof_allocators.h>
2726
#include <proof_helpers/utils.h>
2827

2928
// Stub this until https://github.com/diffblue/cbmc/issues/5344 is fixed
@@ -52,7 +51,7 @@ int generate_enc_materials(
5251
assert(AWS_OBJECT_PTR_IS_WRITABLE(output));
5352
assert(aws_cryptosdk_enc_request_is_valid(request));
5453

55-
struct aws_cryptosdk_enc_materials *materials = can_fail_malloc(sizeof(*materials));
54+
struct aws_cryptosdk_enc_materials *materials = malloc(sizeof(*materials));
5655
if (materials == NULL) {
5756
*output = NULL;
5857
return AWS_OP_ERR;
@@ -107,20 +106,20 @@ void aws_cryptosdk_cmm_generate_enc_materials_harness() {
107106
.decrypt_materials = nondet_voidp() };
108107
__CPROVER_assume(aws_cryptosdk_cmm_vtable_is_valid(&vtable));
109108

110-
struct aws_cryptosdk_cmm *cmm = can_fail_malloc(sizeof(*cmm));
109+
struct aws_cryptosdk_cmm *cmm = malloc(sizeof(*cmm));
111110
__CPROVER_assume(cmm);
112111
cmm->vtable = &vtable;
113112
__CPROVER_assume(aws_cryptosdk_cmm_base_is_valid(cmm));
114113

115-
struct aws_cryptosdk_enc_request *request = can_fail_malloc(sizeof(*request));
114+
struct aws_cryptosdk_enc_request *request = malloc(sizeof(*request));
116115
__CPROVER_assume(request);
117-
request->alloc = can_fail_allocator();
118-
request->enc_ctx = can_fail_malloc(sizeof(*request->enc_ctx));
116+
request->alloc = aws_default_allocator();
117+
request->enc_ctx = malloc(sizeof(*request->enc_ctx));
119118
__CPROVER_assume(request->enc_ctx);
120119
ensure_allocated_hash_table(request->enc_ctx, MAX_NUM_ITEMS);
121120
__CPROVER_assume(aws_cryptosdk_enc_request_is_valid(request));
122121

123-
struct aws_cryptosdk_enc_materials **output = can_fail_malloc(sizeof(*output));
122+
struct aws_cryptosdk_enc_materials **output = malloc(sizeof(*output));
124123
__CPROVER_assume(output);
125124

126125
// Run the function under test.

‎verification/cbmc/proofs/aws_cryptosdk_cmm_release/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,6 @@ PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/atomics.c
3636
PROJECT_SOURCES += $(SRCDIR)/source/materials.c
3737

3838
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
39-
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
4039
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
4140
PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
4241
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

‎verification/cbmc/proofs/aws_cryptosdk_cmm_release/aws_cryptosdk_cmm_release_harness.c

+1-2
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,6 @@
1919
#include <aws/cryptosdk/materials.h>
2020
#include <proof_helpers/cryptosdk/make_common_data_structures.h>
2121
#include <proof_helpers/make_common_data_structures.h>
22-
#include <proof_helpers/proof_allocators.h>
2322
#include <proof_helpers/utils.h>
2423

2524
void destroy(struct aws_cryptosdk_cmm *cmm) {
@@ -36,7 +35,7 @@ void aws_cryptosdk_cmm_release_harness() {
3635
.decrypt_materials = nondet_voidp() };
3736
__CPROVER_assume(aws_cryptosdk_cmm_vtable_is_valid(&vtable));
3837

39-
struct aws_cryptosdk_cmm *cmm = can_fail_malloc(sizeof(struct aws_cryptosdk_cmm));
38+
struct aws_cryptosdk_cmm *cmm = malloc(sizeof(struct aws_cryptosdk_cmm));
4039

4140
if (cmm) {
4241
cmm->vtable = &vtable;

‎verification/cbmc/proofs/aws_cryptosdk_cmm_retain/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,6 @@ PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/atomics.c
3838
PROJECT_SOURCES += $(SRCDIR)/source/materials.c
3939

4040
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
41-
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
4241
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
4342
PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
4443
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

‎verification/cbmc/proofs/aws_cryptosdk_cmm_retain/aws_cryptosdk_cmm_retain_harness.c

-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,6 @@
1919
#include <aws/cryptosdk/materials.h>
2020
#include <proof_helpers/cryptosdk/make_common_data_structures.h>
2121
#include <proof_helpers/make_common_data_structures.h>
22-
#include <proof_helpers/proof_allocators.h>
2322
#include <proof_helpers/utils.h>
2423

2524
void aws_cryptosdk_cmm_retain_harness() {

‎verification/cbmc/proofs/aws_cryptosdk_compare_hash_elems_by_key_string/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -20,13 +20,13 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
2020

2121
CBMCFLAGS +=
2222

23+
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
2324
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
2425
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
2526
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/string.c
2627
PROJECT_SOURCES += $(SRCDIR)/source/utils.c
2728

2829
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
29-
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
3030
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
3131
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
3232
PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c

‎verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -52,8 +52,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/edk.c
5252
PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c
5353
PROJECT_SOURCES += $(SRCDIR)/source/materials.c
5454

55+
PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
5556
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
56-
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
5757
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
5858
PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_table_no_slots_override.c
5959
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

+2-3
Original file line numberDiff line numberDiff line change
@@ -23,13 +23,12 @@
2323
#include <make_common_data_structures.h>
2424
#include <proof_helpers/cryptosdk/make_common_data_structures.h>
2525
#include <proof_helpers/make_common_data_structures.h>
26-
#include <proof_helpers/proof_allocators.h>
2726
#include <proof_helpers/utils.h>
2827

2928
void aws_cryptosdk_dec_materials_destroy_harness() {
30-
struct aws_cryptosdk_dec_materials *materials = can_fail_malloc(sizeof(*materials));
29+
struct aws_cryptosdk_dec_materials *materials = malloc(sizeof(*materials));
3130
if (materials) {
32-
materials->alloc = can_fail_allocator();
31+
materials->alloc = aws_default_allocator();
3332
__CPROVER_assume(aws_allocator_is_valid(materials->alloc));
3433

3534
// Set up the signctx

‎verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -48,8 +48,8 @@ PROJECT_SOURCES += $(SRCDIR)/source/edk.c
4848
PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c
4949
PROJECT_SOURCES += $(SRCDIR)/source/materials.c
5050

51+
PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
5152
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
52-
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
5353
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
5454
PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_table_no_slots_override.c
5555
PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c

‎verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/aws_cryptosdk_dec_materials_new_harness.c

+1-2
Original file line numberDiff line numberDiff line change
@@ -20,11 +20,10 @@
2020
#include <cipher_openssl.h>
2121
#include <proof_helpers/cryptosdk/make_common_data_structures.h>
2222
#include <proof_helpers/make_common_data_structures.h>
23-
#include <proof_helpers/proof_allocators.h>
2423
#include <proof_helpers/utils.h>
2524

2625
void aws_cryptosdk_dec_materials_new_harness() {
27-
struct aws_allocator *alloc = can_fail_allocator();
26+
struct aws_allocator *alloc = aws_default_allocator();
2827
enum aws_cryptosdk_alg_id alg;
2928

3029
struct aws_cryptosdk_dec_materials *rval = aws_cryptosdk_dec_materials_new(alloc, alg);

‎verification/cbmc/proofs/aws_cryptosdk_decrypt_body/Makefile

+3-3
Original file line numberDiff line numberDiff line change
@@ -34,23 +34,23 @@ CBMCFLAGS +=
3434

3535
DEFINES += -DMAX_BUFFER_SIZE=$(MAX_BUFFER_SIZE)
3636

37+
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
3738
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c
3839
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
39-
PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
4040
PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/err_override.c
4141
PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/evp_override.c
4242
PROJECT_SOURCES += $(SRCDIR)/source/cipher.c
4343

4444
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
45-
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
4645
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c
46+
PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
47+
PROOF_SOURCES += $(COMMON_PROOF_UNINLINE)/error.c
4748
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
4849
PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c
4950

5051
REMOVE_FUNCTION_BODY += EVP_EncryptUpdate
5152
REMOVE_FUNCTION_BODY += EVP_sha256
5253
REMOVE_FUNCTION_BODY += EVP_sha384
53-
REMOVE_FUNCTION_BODY += aws_raise_error_private
5454
REMOVE_FUNCTION_BODY += nondet_compare
5555

5656
UNWINDSET += aws_cryptosdk_decrypt_body.0:$(call addone,$(MAX_BUFFER_SIZE))

‎verification/cbmc/proofs/aws_cryptosdk_decrypt_body/aws_cryptosdk_decrypt_body_harness.c

+5-5
Original file line numberDiff line numberDiff line change
@@ -22,33 +22,33 @@ void aws_cryptosdk_decrypt_body_harness() {
2222
struct aws_cryptosdk_alg_properties *props = aws_cryptosdk_alg_props(alg_id);
2323
__CPROVER_assume(aws_cryptosdk_alg_properties_is_valid(props));
2424

25-
struct aws_byte_buf *outp = can_fail_malloc(sizeof(*outp));
25+
struct aws_byte_buf *outp = malloc(sizeof(*outp));
2626
__CPROVER_assume(outp != NULL);
2727
__CPROVER_assume(aws_byte_buf_is_bounded(outp, MAX_BUFFER_SIZE));
2828
ensure_byte_buf_has_allocated_buffer_member(outp);
2929
__CPROVER_assume(aws_byte_buf_is_valid(outp));
3030

31-
struct aws_byte_cursor *inp = can_fail_malloc(sizeof(*inp));
31+
struct aws_byte_cursor *inp = malloc(sizeof(*inp));
3232
__CPROVER_assume(inp != NULL);
3333
__CPROVER_assume(aws_byte_cursor_is_bounded(inp, MAX_BUFFER_SIZE));
3434
ensure_byte_cursor_has_allocated_buffer_member(inp);
3535
__CPROVER_assume(aws_byte_cursor_is_valid(inp));
3636

37-
struct aws_byte_buf *message_id = can_fail_malloc(sizeof(*message_id));
37+
struct aws_byte_buf *message_id = malloc(sizeof(*message_id));
3838
__CPROVER_assume(message_id != NULL);
3939
__CPROVER_assume(aws_byte_buf_is_bounded(message_id, MAX_BUFFER_SIZE));
4040
ensure_byte_buf_has_allocated_buffer_member(message_id);
4141
__CPROVER_assume(aws_byte_buf_is_valid(message_id));
4242

4343
uint32_t seqno;
4444

45-
uint8_t *iv = can_fail_malloc(props->iv_len);
45+
uint8_t *iv = malloc(props->iv_len);
4646
__CPROVER_assume(iv != NULL);
4747

4848
struct content_key *content_key;
4949

5050
/* Need to allocate tag_len bytes for writing the tag */
51-
uint8_t *tag = can_fail_malloc(props->tag_len);
51+
uint8_t *tag = malloc(props->tag_len);
5252
__CPROVER_assume(tag != NULL);
5353

5454
int body_frame_type;

‎verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/Makefile

+2-1
Original file line numberDiff line numberDiff line change
@@ -29,10 +29,11 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
2929
CBMCFLAGS +=
3030

3131
PROJECT_SOURCES += $(SRCDIR)/source/default_cmm.c
32+
PROJECT_SOURCES += $(SRCDIR)/source/header.c
3233
PROJECT_SOURCES += $(SRCDIR)/source/materials.c
3334

35+
PROOF_SOURCES += $(CBMC_ROOT)/aws-c-common/source/allocator.c
3436
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
35-
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
3637
PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
3738
PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c
3839
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

‎verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/aws_cryptosdk_default_cmm_set_alg_id_harness.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ void aws_cryptosdk_default_cmm_set_alg_id_harness() {
3535
__CPROVER_assume(aws_cryptosdk_keyring_is_valid(keyring));
3636

3737
/* Instantiate the default (non-caching) implementation of the Crypto MaterialsManager (CMM) */
38-
struct aws_cryptosdk_cmm *cmm = aws_cryptosdk_default_cmm_new(can_fail_allocator(), keyring);
38+
struct aws_cryptosdk_cmm *cmm = aws_cryptosdk_default_cmm_new(aws_default_allocator(), keyring);
3939

4040
/* Assumptions */
4141
__CPROVER_assume(cmm != NULL);

‎verification/cbmc/proofs/aws_cryptosdk_deserialize_frame/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,6 @@ PROJECT_SOURCES += $(SRCDIR)/source/cipher.c
2929
PROJECT_SOURCES += $(SRCDIR)/source/framefmt.c
3030

3131
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c
32-
PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c
3332
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
3433
PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c
3534
###########

0 commit comments

Comments
 (0)