Skip to content

Commit 5cc2830

Browse files
tegansbdanielsnfeliperodri
authored
Applies malloc flags across all CBMC proofs (#619)
* Updated proofs harnesses for aws_cryptosdk_rsa_encrypt and decrypt (#603) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Update c-common to latest, and update the makefile to match * fixed keyring_trace_add_record_buf and keyring_on_encrypt * push c-common again, and fix makefile for aws_gcm_decypt * Updated harneses with explicit non-NULL assumptions to handle may-fail-malloc flag Added preconditions to source code * Use new string allocators and add matching preconditions to harness Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Updates to aws_atomic_var_is_valid and aws_cryptosdk_keyring_base_init harness (#607) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Update c-common to latest, and update the makefile to match * fixed keyring_trace_add_record_buf and keyring_on_encrypt * push c-common again, and fix makefile for aws_gcm_decypt * Added non-NULL assumptions to keyring_base_init harness for vtable name modified aws_atomic_var_is_valid check Fixed IMPLIES structure of assume Fix comment structure in cmm_base_init harness aws_atomic_var_is_valid divided into two functions, one for int and one for ptr, preconditions added to source code Updated Makefile to include MAX_STRING_LEN update to keyring_on_encrypt and keyring_on_decrypt proof harnesses * Added the ensure_vtable_has_allocated_members function * Use ensures function in the harness as well as bounded malloc * removed unneeded assumption on refcount.value * Removed stubs from Makefile * use malloc and ensure_vtable_has_allocated_members * Use new ensure_nondet_allocate_vtable_members function * Made two vtable allocator functions, for keyring_trace and cmm Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Update harness for aws_cryptosdk_enc_ctx_clone (#611) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Update c-common to latest, and update the makefile to match * fixed keyring_trace_add_record_buf and keyring_on_encrypt * push c-common again, and fix makefile for aws_gcm_decypt * Update enc_ctx_clone harness and Makefile, additional assumptions, needs new stubs from aws-c-common * Updated harness to use malloc * update time in Makefile and remove unneeded assumptions Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Update to aws_cryptosdk_enc_ctx_size proof (#608) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Update c-common to latest, and update the makefile to match * fixed keyring_trace_add_record_buf and keyring_on_encrypt * push c-common again, and fix makefile for aws_gcm_decypt * Updated harness for enc_ctx_size and added non-NULL assumptions * Malloc data structures and then assume non-NULL * Use aws_string_is_valid and added preconditions to source code * Updated conditions in the function to asserts * include missing assert header * size becomes *size Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Update CBMC harnesses for aws_cryptosdk_enc_ctx_serialize, aws_cryptosdk_sig_sign_start and aws_cryptosdk_sig_get_privkey (#606) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Update c-common to latest, and update the makefile to match * fixed keyring_trace_add_record_buf and keyring_on_encrypt * push c-common again, and fix makefile for aws_gcm_decypt * Simple cleanup of sig_get_privkey harness Added explicit non-NULL instructions to sig_sign_start harness Added explicit non-NULL assumptions to the key and value fiends of each array_list_element in enc_ctx_serialize harness Added corresponding preconditions to source code functions * Added ensure_sig_ctx_has_allocated_members function and harness updates * Updated preconditions in the source code * Updated other harnesses to use the new ensure_sig_ctx_has_allocated_members function * Use malloc * rename of ensure_sig_ctx_has_allocated_members function * change function name * Update to aws_cryptosdk_dec_materials_destroy and enc_material_destroy harnesses * fixes * Added precondition to source code * remove memory leak check from Makefile remove memory clean up moved assumptions about non-NULL elems remove memory leak check from .yaml Added comment about non-NULL assumption in hash_elems * Removed too strong assumption about privkey Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Updates aws_cryptosdk_keyring_trace_copy_all proof (#609) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Update c-common to latest, and update the makefile to match * fixed keyring_trace_add_record_buf and keyring_on_encrypt * push c-common again, and fix makefile for aws_gcm_decypt * Updated harness for keyring_trace_copy_all to handle new malloc-may-fail flag Added new ensure_trace_has_readable_records function Updated Makefile with loop unwinding Added preconditions to source code update to new c-common revert to old aws-c-common * Use malloc instead of can-fail * update to recent c common to see if proof will go through CI * use the aws_cryptosdk_keyring_trace_is_valid function and update yaml * remove extra function from make_common_datastructures Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Update aws_cryptodsk_sig_verify_start and aws_cryptodsk_sig_verify_finish harnesses (#602) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Updated assumptions in proof harnesses to handle malloc-may-fail Updated preconditions in source code to match those in harness * updates and use the ensure_sig_ctx_has_allocated_members function * Added is_valid assumptions to source code * update signature * Simple cleanup of sig_get_privkey harness Added explicit non-NULL instructions to sig_sign_start harness Added explicit non-NULL assumptions to the key and value fiends of each array_list_element in enc_ctx_serialize harness Added corresponding preconditions to source code functions * Added ensure_sig_ctx_has_allocated_members function and harness updates * Updated preconditions in the source code * Remove un-needed assumptions Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Update harnesses for keyring_trace_add_record, keyring_trace_add_record_c_str and aws_cryptosdk_keyring_trace_record_init_clone (#604) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Update c-common to latest, and update the makefile to match * fixed keyring_trace_add_record_buf and keyring_on_encrypt * push c-common again, and fix makefile for aws_gcm_decypt * Update harnesses with non-NULL assumptions on strings Added non-NULL assumptions on strings to harness * Updated harnesses to use is_valid assumptions, new c-common allocation functions and matched preconditions in the source code * Use ensure_string_is_allocated_nondet_length for record_init_clone and assumption on length * Fixed changes to ensure_record_has_allocated_members * Fixed broken proofs due to changes in c-common not addressed in other PRs * update harness for string_dup and compare_hash_elems_by_key_string * Update to c-common Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Update harness for edk_list_copy_all (#610) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Update c-common to latest, and update the makefile to match * fixed keyring_trace_add_record_buf and keyring_on_encrypt * push c-common again, and fix makefile for aws_gcm_decypt * Added the ensure_cryptosdk_edk_list_elements_are_readable function Updated edk_list_copy_all harness with assumptions for the malloc-may-fail flag Added to unwindset Added preconditions to source code * use malloc * Update to use aws_cryptosdk_edk_list_elements_are_valid Updated signature for clean up and init stubs Updated signature for clean up and init stubs add yaml Update signature for clean_up and init_clone * Update Makefile * Update to new c-common and remove un-needed function * set NUM_ELEMS to 1 just to test * Stub out aws_array_list_push_back and aws_array_list_pop_back * Updated time comment in Makefile Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Update Makefile.common with malloc-may-fail and malloc-fail-null (#618) * Removes extra flags from coverage check (#617) Signed-off-by: Felipe R. Monteiro <[email protected]> * Improves coverage for the aws_cryptosdk_md_* proofs (#616) * Added READMEs documenting expected coverage for aws_cryptosdk_md_update and aws_cryptosdk_md_abort * Added stubs for EVP_MD_CTX_free and evp_md_ctx_is_valid to be used when ctx->pkey is sure to be NULL * Updated Makefile to use new stubs for EVP_MD_XTX_free and evp_md_ctx_is_valid to improve coverage * Updated README.md files with new expected coverage * Use AWS_FATAL_PRECONDITION instead of abort * Updated Makefiles with stubs for aws_raise_error_private, EVP_MD_CTX_free and evp_md_ctx_is_valid * Added README files specifying expected coverage behavior * Empty commit to run tests * Empty commit to run tests * More descriptive names for stubs and added documentation to Makefile * Added additional documentation to Makefile and updated stub names * Added more information about unreached lines of code * Moved struct definitions for evp_md_ctx_st and evp_pkey_st to evp.h * Use AWS_FATAL_PRECONDITION instead of abort * Updated Makefiles with stubs for aws_raise_error_private, EVP_MD_CTX_free and evp_md_ctx_is_valid * Added README files specifying expected coverage behavior * Added additional documentation to Makefile and updated stub names * Added more information about unreached lines of code * Re-ordered structs in evp.h and fixed comments * remove extra line * Removed unneeded includes and cleaned comments * made pkey == NULL into an assert * Remove unnecessary READMEs for proofs with full coverage * Added comments about abstractions and removed REMOVE_FUNCTION_BODIES * Use AWS_FATAL_PRECONDITION instead of abort * Updated Makefiles with stubs for aws_raise_error_private, EVP_MD_CTX_free and evp_md_ctx_is_valid * Added README files specifying expected coverage behavior * Added additional documentation to Makefile and updated stub names * Added more information about unreached lines of code * Removed extra line in Makefiles * Remove README for function with full coverage * Removed redition of struct from stubs * empty commit to rerun tests * Simplified includes for stubs * Trigger CI * Trigger stuck CI Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> Co-authored-by: Felipe R. Monteiro <[email protected]> * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Updated proofs harnesses for aws_cryptosdk_rsa_encrypt and decrypt (#603) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Update c-common to latest, and update the makefile to match * fixed keyring_trace_add_record_buf and keyring_on_encrypt * push c-common again, and fix makefile for aws_gcm_decypt * Updated harneses with explicit non-NULL assumptions to handle may-fail-malloc flag Added preconditions to source code * Use new string allocators and add matching preconditions to harness Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Updates to aws_atomic_var_is_valid and aws_cryptosdk_keyring_base_init harness (#607) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Update c-common to latest, and update the makefile to match * fixed keyring_trace_add_record_buf and keyring_on_encrypt * push c-common again, and fix makefile for aws_gcm_decypt * Added non-NULL assumptions to keyring_base_init harness for vtable name modified aws_atomic_var_is_valid check Fixed IMPLIES structure of assume Fix comment structure in cmm_base_init harness aws_atomic_var_is_valid divided into two functions, one for int and one for ptr, preconditions added to source code Updated Makefile to include MAX_STRING_LEN update to keyring_on_encrypt and keyring_on_decrypt proof harnesses * Added the ensure_vtable_has_allocated_members function * Use ensures function in the harness as well as bounded malloc * removed unneeded assumption on refcount.value * Removed stubs from Makefile * use malloc and ensure_vtable_has_allocated_members * Use new ensure_nondet_allocate_vtable_members function * Made two vtable allocator functions, for keyring_trace and cmm Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Update harness for aws_cryptosdk_enc_ctx_clone (#611) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Update c-common to latest, and update the makefile to match * fixed keyring_trace_add_record_buf and keyring_on_encrypt * push c-common again, and fix makefile for aws_gcm_decypt * Update enc_ctx_clone harness and Makefile, additional assumptions, needs new stubs from aws-c-common * Updated harness to use malloc * update time in Makefile and remove unneeded assumptions Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Update to aws_cryptosdk_enc_ctx_size proof (#608) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Update c-common to latest, and update the makefile to match * fixed keyring_trace_add_record_buf and keyring_on_encrypt * push c-common again, and fix makefile for aws_gcm_decypt * Updated harness for enc_ctx_size and added non-NULL assumptions * Malloc data structures and then assume non-NULL * Use aws_string_is_valid and added preconditions to source code * Updated conditions in the function to asserts * include missing assert header * size becomes *size Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Update CBMC harnesses for aws_cryptosdk_enc_ctx_serialize, aws_cryptosdk_sig_sign_start and aws_cryptosdk_sig_get_privkey (#606) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Update c-common to latest, and update the makefile to match * fixed keyring_trace_add_record_buf and keyring_on_encrypt * push c-common again, and fix makefile for aws_gcm_decypt * Simple cleanup of sig_get_privkey harness Added explicit non-NULL instructions to sig_sign_start harness Added explicit non-NULL assumptions to the key and value fiends of each array_list_element in enc_ctx_serialize harness Added corresponding preconditions to source code functions * Added ensure_sig_ctx_has_allocated_members function and harness updates * Updated preconditions in the source code * Updated other harnesses to use the new ensure_sig_ctx_has_allocated_members function * Use malloc * rename of ensure_sig_ctx_has_allocated_members function * change function name * Update to aws_cryptosdk_dec_materials_destroy and enc_material_destroy harnesses * fixes * Added precondition to source code * remove memory leak check from Makefile remove memory clean up moved assumptions about non-NULL elems remove memory leak check from .yaml Added comment about non-NULL assumption in hash_elems * Removed too strong assumption about privkey Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Updates aws_cryptosdk_keyring_trace_copy_all proof (#609) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Update c-common to latest, and update the makefile to match * fixed keyring_trace_add_record_buf and keyring_on_encrypt * push c-common again, and fix makefile for aws_gcm_decypt * Updated harness for keyring_trace_copy_all to handle new malloc-may-fail flag Added new ensure_trace_has_readable_records function Updated Makefile with loop unwinding Added preconditions to source code update to new c-common revert to old aws-c-common * Use malloc instead of can-fail * update to recent c common to see if proof will go through CI * use the aws_cryptosdk_keyring_trace_is_valid function and update yaml * remove extra function from make_common_datastructures Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Update aws_cryptodsk_sig_verify_start and aws_cryptodsk_sig_verify_finish harnesses (#602) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Updated assumptions in proof harnesses to handle malloc-may-fail Updated preconditions in source code to match those in harness * updates and use the ensure_sig_ctx_has_allocated_members function * Added is_valid assumptions to source code * update signature * Simple cleanup of sig_get_privkey harness Added explicit non-NULL instructions to sig_sign_start harness Added explicit non-NULL assumptions to the key and value fiends of each array_list_element in enc_ctx_serialize harness Added corresponding preconditions to source code functions * Added ensure_sig_ctx_has_allocated_members function and harness updates * Updated preconditions in the source code * Remove un-needed assumptions Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Update Makefile.common with -malloc-may-fail and ---malloc-fail-null flags * Update harnesses for keyring_trace_add_record, keyring_trace_add_record_c_str and aws_cryptosdk_keyring_trace_record_init_clone (#604) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Update c-common to latest, and update the makefile to match * fixed keyring_trace_add_record_buf and keyring_on_encrypt * push c-common again, and fix makefile for aws_gcm_decypt * Update harnesses with non-NULL assumptions on strings Added non-NULL assumptions on strings to harness * Updated harnesses to use is_valid assumptions, new c-common allocation functions and matched preconditions in the source code * Use ensure_string_is_allocated_nondet_length for record_init_clone and assumption on length * Fixed changes to ensure_record_has_allocated_members * Fixed broken proofs due to changes in c-common not addressed in other PRs * update harness for string_dup and compare_hash_elems_by_key_string * Update to c-common Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Update harness for edk_list_copy_all (#610) * Make c-common a submodule for verification, and update the CBMC makefile to point at it * Update c-common to latest, and update the makefile to match * fixed keyring_trace_add_record_buf and keyring_on_encrypt * push c-common again, and fix makefile for aws_gcm_decypt * Added the ensure_cryptosdk_edk_list_elements_are_readable function Updated edk_list_copy_all harness with assumptions for the malloc-may-fail flag Added to unwindset Added preconditions to source code * use malloc * Update to use aws_cryptosdk_edk_list_elements_are_valid Updated signature for clean up and init stubs Updated signature for clean up and init stubs add yaml Update signature for clean_up and init_clone * Update Makefile * Update to new c-common and remove un-needed function * set NUM_ELEMS to 1 just to test * Stub out aws_array_list_push_back and aws_array_list_pop_back * Updated time comment in Makefile Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> * Pushing new yamls and updating Makefile * Update Makefiles for enc_materials_new and dec_materials_new and harness for enc_ctx_deserialize * update c-common Co-authored-by: Felipe R. Monteiro <[email protected]> Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> Co-authored-by: Felipe R. Monteiro <[email protected]> Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>
1 parent f73e54e commit 5cc2830

File tree

121 files changed

+450
-325
lines changed

Some content is hidden

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

121 files changed

+450
-325
lines changed

‎.cbmc-batch/aws-c-common

Submodule aws-c-common updated 64 files

‎.cbmc-batch/include/make_common_data_structures.h

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ void ensure_alg_properties_attempt_allocation(struct aws_cryptosdk_alg_propertie
3030
void ensure_md_context_has_allocated_members(struct aws_cryptosdk_md_context *ctx);
3131

3232
/* Allocates the members of the context and ensures that internal pointers are pointing to the correct objects. */
33-
void ensure_sig_ctx_has_allocated_members(struct aws_cryptosdk_sig_ctx *ctx);
33+
struct aws_cryptosdk_sig_ctx *ensure_nondet_sig_ctx_has_allocated_members();
3434

3535
bool aws_cryptosdk_edk_list_is_bounded(
3636
const struct aws_array_list *const list, const size_t max_initial_item_allocation);
@@ -47,3 +47,7 @@ void ensure_trace_has_allocated_records(struct aws_array_list *trace, size_t max
4747
/* Non-deterministically allocates a aws_cryptosdk_keyring structure */
4848
void ensure_cryptosdk_keyring_has_allocated_members(
4949
struct aws_cryptosdk_keyring *keyring, const struct aws_cryptosdk_keyring_vt *vtable);
50+
/* Non-deterministically allocates a aws_cryptosdk_keyring_vt structure with a valid name*/
51+
void ensure_nondet_allocate_keyring_vtable_members(struct aws_cryptosdk_keyring_vt *vtable, size_t max_len);
52+
/* Non-deterministically allocates a aws_cryptosdk_cmm_vt structure with a valid name*/
53+
void ensure_nondet_allocate_cmm_vtable_members(struct aws_cryptosdk_cmm_vt *vtable, size_t max_len);

‎.cbmc-batch/jobs/Makefile.common

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,8 @@ CHECKFLAGS += --signed-overflow-check
6161
CHECKFLAGS += --undefined-shift-check
6262
CHECKFLAGS += --unsigned-overflow-check
6363
CHECKFLAGS += --unwinding-assertions
64+
CHECKFLAGS += --malloc-may-fail
65+
CHECKFLAGS += --malloc-fail-null
6466

6567
CBMCFLAGS += $(CHECKFLAGS)
6668

@@ -276,7 +278,7 @@ property.xml: $(ENTRY).goto
276278
cbmc $(CBMCFLAGS) --show-properties --xml-ui $< 2>&1 > $@
277279

278280
coverage.xml: $(ENTRY).goto
279-
cbmc $(filter-out $(CHECKFLAGS),$(CBMCFLAGS)) --cover location --xml-ui $< 2>&1 > $@
281+
cbmc $(filter-out $(CHECKFLAGS),$(CBMCFLAGS)) --malloc-may-fail --malloc-fail-null --cover location --xml-ui $< 2>&1 > $@
280282

281283
cbmc: cbmc.log
282284

‎.cbmc-batch/jobs/aws_cryptosdk_aes_gcm_decrypt/cbmc-batch.yaml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
jobos: ubuntu16
2-
cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;flush_openssl_errors.0:1;--object-bits;8"
3-
goto: aws_cryptosdk_aes_gcm_decrypt_harness.goto
1+
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;flush_openssl_errors.0:1;--object-bits;8"
42
expected: "SUCCESSFUL"
3+
goto: aws_cryptosdk_aes_gcm_decrypt_harness.goto
4+
jobos: ubuntu16

‎.cbmc-batch/jobs/aws_cryptosdk_aes_gcm_encrypt/cbmc-batch.yaml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
jobos: ubuntu16
2-
cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;flush_openssl_errors.0:1;--object-bits;8"
3-
goto: aws_cryptosdk_aes_gcm_encrypt_harness.goto
1+
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;flush_openssl_errors.0:1;--object-bits;8"
42
expected: "SUCCESSFUL"
3+
goto: aws_cryptosdk_aes_gcm_encrypt_harness.goto
4+
jobos: ubuntu16

‎.cbmc-batch/jobs/aws_cryptosdk_alg_props/cbmc-batch.yaml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
cbmcflags: "--flush;--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
1+
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8"
22
expected: "SUCCESSFUL"
33
goto: aws_cryptosdk_alg_props_harness.goto
44
jobos: ubuntu16

‎.cbmc-batch/jobs/aws_cryptosdk_cmm_base_init/aws_cryptosdk_cmm_base_init_harness.c

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,16 +17,23 @@
1717
*/
1818

1919
#include <aws/cryptosdk/materials.h>
20-
#include <proof_helpers/cryptosdk/make_common_data_structures.h>
20+
#include <make_common_data_structures.h>
2121
#include <proof_helpers/make_common_data_structures.h>
2222
#include <proof_helpers/proof_allocators.h>
2323
#include <proof_helpers/utils.h>
2424

2525
void aws_cryptosdk_cmm_base_init_harness() {
26+
/* Nondet input */
2627
struct aws_cryptosdk_cmm cmm;
2728
const struct aws_cryptosdk_cmm_vt vtable;
28-
*(char **)(&vtable.name) = ensure_c_str_is_allocated(SIZE_MAX);
29+
30+
/* Assumptions */
31+
ensure_nondet_allocate_cmm_vtable_members(&vtable, SIZE_MAX);
2932
__CPROVER_assume(aws_cryptosdk_cmm_vtable_is_valid(&vtable));
33+
34+
/* Operation under verification */
3035
aws_cryptosdk_cmm_base_init(&cmm, &vtable);
36+
37+
/* Post-conditions */
3138
assert(aws_cryptosdk_cmm_base_is_valid(&cmm));
3239
}

‎.cbmc-batch/jobs/aws_cryptosdk_cmm_base_init/cbmc-batch.yaml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
jobos: ubuntu16
2-
cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
3-
goto: aws_cryptosdk_cmm_base_init_harness.goto
1+
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8"
42
expected: "SUCCESSFUL"
3+
goto: aws_cryptosdk_cmm_base_init_harness.goto
4+
jobos: ubuntu16

‎.cbmc-batch/jobs/aws_cryptosdk_cmm_decrypt_materials/aws_cryptosdk_cmm_decrypt_materials_harness.c

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -77,11 +77,8 @@ int decrypt_materials(
7777
__CPROVER_assume(aws_cryptosdk_keyring_trace_is_valid(&materials->keyring_trace));
7878

7979
// Set up the signctx
80-
materials->signctx = can_fail_malloc(sizeof(*materials->signctx));
81-
if (materials->signctx) {
82-
ensure_sig_ctx_has_allocated_members(materials->signctx);
83-
__CPROVER_assume(aws_cryptosdk_sig_ctx_is_valid_cbmc(materials->signctx));
84-
}
80+
materials->signctx = ensure_nondet_sig_ctx_has_allocated_members();
81+
__CPROVER_assume(aws_cryptosdk_sig_ctx_is_valid_cbmc(materials->signctx));
8582

8683
*output = materials;
8784
return AWS_OP_SUCCESS;

‎.cbmc-batch/jobs/aws_cryptosdk_cmm_decrypt_materials/cbmc-batch.yaml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;aws_cryptosdk_edk_list_clear.0:2,aws_cryptosdk_edk_list_elements_are_bounded.0:2,aws_cryptosdk_edk_list_elements_are_valid.0:2,aws_cryptosdk_edk_list_is_bounded.0:2,aws_cryptosdk_edk_list_is_valid.0:2,aws_cryptosdk_keyring_trace_clear.0:2,aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:2,ensure_cryptosdk_edk_list_has_allocated_members.0:2,ensure_trace_has_allocated_records.0:2;--object-bits;8"
1+
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_edk_list_clear.0:2,aws_cryptosdk_edk_list_elements_are_bounded.0:2,aws_cryptosdk_edk_list_elements_are_valid.0:2,aws_cryptosdk_edk_list_is_bounded.0:2,aws_cryptosdk_edk_list_is_valid.0:2,aws_cryptosdk_keyring_trace_clear.0:2,aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:2,ensure_cryptosdk_edk_list_has_allocated_members.0:2,ensure_trace_has_allocated_records.0:2;--object-bits;8"
22
expected: "SUCCESSFUL"
33
goto: aws_cryptosdk_cmm_decrypt_materials_harness.goto
44
jobos: ubuntu16

‎.cbmc-batch/jobs/aws_cryptosdk_cmm_generate_enc_materials/aws_cryptosdk_cmm_generate_enc_materials_harness.c

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -63,11 +63,8 @@ int generate_enc_materials(
6363
__CPROVER_assume(aws_allocator_is_valid(materials->alloc));
6464

6565
// Set up the signctx
66-
materials->signctx = can_fail_malloc(sizeof(*materials->signctx));
67-
if (materials->signctx) {
68-
ensure_sig_ctx_has_allocated_members(materials->signctx);
69-
__CPROVER_assume(aws_cryptosdk_sig_ctx_is_valid_cbmc(materials->signctx));
70-
}
66+
materials->signctx = ensure_nondet_sig_ctx_has_allocated_members();
67+
__CPROVER_assume(aws_cryptosdk_sig_ctx_is_valid_cbmc(materials->signctx));
7168

7269
// Set up the unencrypted_data_key
7370
__CPROVER_assume(aws_byte_buf_is_bounded(&materials->unencrypted_data_key, MAX_NUM_ITEMS));

‎.cbmc-batch/jobs/aws_cryptosdk_cmm_generate_enc_materials/cbmc-batch.yaml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;aws_cryptosdk_edk_list_clear.0:2,aws_cryptosdk_edk_list_elements_are_bounded.0:2,aws_cryptosdk_edk_list_elements_are_valid.0:2,aws_cryptosdk_edk_list_is_bounded.0:2,aws_cryptosdk_edk_list_is_valid.0:2,aws_cryptosdk_keyring_trace_clear.0:2,aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:2,ensure_cryptosdk_edk_list_has_allocated_members.0:2,ensure_trace_has_allocated_records.0:2;--object-bits;8"
1+
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_edk_list_clear.0:2,aws_cryptosdk_edk_list_elements_are_bounded.0:2,aws_cryptosdk_edk_list_elements_are_valid.0:2,aws_cryptosdk_edk_list_is_bounded.0:2,aws_cryptosdk_edk_list_is_valid.0:2,aws_cryptosdk_keyring_trace_clear.0:2,aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:2,ensure_cryptosdk_edk_list_has_allocated_members.0:2,ensure_trace_has_allocated_records.0:2;--object-bits;8"
22
expected: "SUCCESSFUL"
33
goto: aws_cryptosdk_cmm_generate_enc_materials_harness.goto
44
jobos: ubuntu16

‎.cbmc-batch/jobs/aws_cryptosdk_cmm_release/cbmc-batch.yaml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
1+
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8"
22
expected: "SUCCESSFUL"
33
goto: aws_cryptosdk_cmm_release_harness.goto
44
jobos: ubuntu16

‎.cbmc-batch/jobs/aws_cryptosdk_cmm_retain/cbmc-batch.yaml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
jobos: ubuntu16
2-
cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
3-
goto: aws_cryptosdk_cmm_retain_harness.goto
1+
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8"
42
expected: "SUCCESSFUL"
3+
goto: aws_cryptosdk_cmm_retain_harness.goto
4+
jobos: ubuntu16

‎.cbmc-batch/jobs/aws_cryptosdk_compare_hash_elems_by_key_string/aws_cryptosdk_compare_hash_elems_by_key_string_harness.c

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -19,11 +19,13 @@
1919
#include <proof_helpers/utils.h>
2020

2121
struct aws_hash_element *nondet_hash_string_element_allocation(size_t max_size) {
22-
struct aws_hash_element *elem = can_fail_malloc(sizeof(*elem));
22+
struct aws_hash_element *elem = malloc(sizeof(*elem));
2323
if (elem != NULL) {
2424
if (nondet_bool()) {
25-
elem->key = ensure_string_is_allocated_bounded_length(max_size);
26-
__CPROVER_assume(aws_string_is_valid(elem->key));
25+
struct aws_string *key = ensure_string_is_allocated_nondet_length();
26+
__CPROVER_assume(aws_string_is_valid(key));
27+
__CPROVER_assume(key->len <= max_size);
28+
elem->key = key;
2729
} else {
2830
elem->key = NULL;
2931
}

‎.cbmc-batch/jobs/aws_cryptosdk_compare_hash_elems_by_key_string/cbmc-batch.yaml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;memcmp.0:17;--object-bits;8"
1+
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwindset;memcmp.0:17;--object-bits;8"
22
expected: "SUCCESSFUL"
33
goto: aws_cryptosdk_compare_hash_elems_by_key_string_harness.goto
44
jobos: ubuntu16

‎.cbmc-batch/jobs/aws_cryptosdk_dec_materials_destroy/aws_cryptosdk_dec_materials_destroy_harness.c

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -33,11 +33,8 @@ void aws_cryptosdk_dec_materials_destroy_harness() {
3333
__CPROVER_assume(aws_allocator_is_valid(materials->alloc));
3434

3535
// Set up the signctx
36-
materials->signctx = can_fail_malloc(sizeof(*materials->signctx));
37-
if (materials->signctx) {
38-
ensure_sig_ctx_has_allocated_members(materials->signctx);
39-
__CPROVER_assume(aws_cryptosdk_sig_ctx_is_valid_cbmc(materials->signctx));
40-
}
36+
materials->signctx = ensure_nondet_sig_ctx_has_allocated_members();
37+
__CPROVER_assume(aws_cryptosdk_sig_ctx_is_valid_cbmc(materials->signctx));
4138

4239
// Set up the unencrypted_data_key
4340
__CPROVER_assume(aws_byte_buf_is_bounded(&materials->unencrypted_data_key, MAX_NUM_ITEMS));

‎.cbmc-batch/jobs/aws_cryptosdk_dec_materials_destroy/cbmc-batch.yaml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_trace_has_allocated_records.0:2,aws_cryptosdk_keyring_trace_clear.0:2;--object-bits;8"
1+
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_trace_has_allocated_records.0:2,aws_cryptosdk_keyring_trace_clear.0:2;--object-bits;8"
22
expected: "SUCCESSFUL"
33
goto: aws_cryptosdk_dec_materials_destroy_harness.goto
44
jobos: ubuntu16

‎.cbmc-batch/jobs/aws_cryptosdk_dec_materials_new/Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ include ../Makefile.string
2222
#########
2323
# Local vars
2424
# Expected runtime 2min
25+
KEYRING_TRACE_SIZE = 10 # Value is hardcoded in aws_cryptosdk_keyring_trace_init
2526

2627
#########
2728
ABSTRACTIONS += $(SRCDIR)/c-common-helper-stubs/error.c
@@ -50,5 +51,6 @@ DEPENDENCIES += $(SRCDIR)/c-common-helper-uninline/atomics.c
5051

5152
ENTRY = aws_cryptosdk_dec_materials_new_harness
5253

54+
UNWINDSET += aws_cryptosdk_keyring_trace_is_valid.0:$(shell echo $$(($(KEYRING_TRACE_SIZE) + 1)))
5355
###########
5456
include ../Makefile.common

‎.cbmc-batch/jobs/aws_cryptosdk_dec_materials_new/cbmc-batch.yaml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
1+
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_keyring_trace_is_valid.0:11;--object-bits;8"
22
expected: "SUCCESSFUL"
33
goto: aws_cryptosdk_dec_materials_new_harness.goto
44
jobos: ubuntu16

‎.cbmc-batch/jobs/aws_cryptosdk_decrypt_body/cbmc-batch.yaml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;aws_cryptosdk_decrypt_body.0:5,strlen.0:37;--object-bits;8"
1+
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_decrypt_body.0:5,strlen.0:37;--object-bits;8"
22
expected: "SUCCESSFUL"
33
goto: aws_cryptosdk_decrypt_body_harness.goto
44
jobos: ubuntu16

‎.cbmc-batch/jobs/aws_cryptosdk_derive_key/cbmc-batch.yaml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
cbmcflags: "--flush;--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
1+
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8"
22
expected: "SUCCESSFUL"
33
goto: aws_cryptosdk_derive_key_harness.goto
44
jobos: ubuntu16

‎.cbmc-batch/jobs/aws_cryptosdk_deserialize_frame/cbmc-batch.yaml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
jobos: ubuntu16
2-
cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
3-
goto: aws_cryptosdk_deserialize_frame_harness.goto
1+
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8"
42
expected: "SUCCESSFUL"
3+
goto: aws_cryptosdk_deserialize_frame_harness.goto
4+
jobos: ubuntu16

‎.cbmc-batch/jobs/aws_cryptosdk_edk_clean_up/cbmc-batch.yaml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
jobos: ubuntu16
2-
cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
3-
goto: aws_cryptosdk_edk_clean_up_harness.goto
1+
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8"
42
expected: "SUCCESSFUL"
3+
goto: aws_cryptosdk_edk_clean_up_harness.goto
4+
jobos: ubuntu16

‎.cbmc-batch/jobs/aws_cryptosdk_edk_eq/cbmc-batch.yaml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
jobos: ubuntu16
2-
cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
3-
goto: aws_cryptosdk_edk_eq_harness.goto
1+
cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8"
42
expected: "SUCCESSFUL"
3+
goto: aws_cryptosdk_edk_eq_harness.goto
4+
jobos: ubuntu16

0 commit comments

Comments
 (0)