Path	Lines of Code
verification/cbmc/check_result.py	31
verification/cbmc/cipher_proofs.c	27
verification/cbmc/config.h	1
verification/cbmc/hdr_zeroize.c	24
verification/cbmc/header_proofs.c	100
verification/cbmc/include/aws/common/config.h	1
verification/cbmc/include/aws/cryptosdk/private/config.h	1
verification/cbmc/include/bn_utils.h	7
verification/cbmc/include/cbmc_invariants.h	6
verification/cbmc/include/cipher_openssl.h	18
verification/cbmc/include/ec_utils.h	19
verification/cbmc/include/evp_utils.h	16
verification/cbmc/include/make_common_data_structures.h	57
verification/cbmc/include/openssl/asn1.h	9
verification/cbmc/include/openssl/bio.h	19
verification/cbmc/include/openssl/bn.h	9
verification/cbmc/include/openssl/crypto.h	1
verification/cbmc/include/openssl/ec.h	35
verification/cbmc/include/openssl/ecdsa.h	1
verification/cbmc/include/openssl/err.h	7
verification/cbmc/include/openssl/evp.h	111
verification/cbmc/include/openssl/hmac.h	10
verification/cbmc/include/openssl/kdf.h	40
verification/cbmc/include/openssl/objects.h	7
verification/cbmc/include/openssl/opensslv.h	4
verification/cbmc/include/openssl/ossl_typ.h	23
verification/cbmc/include/openssl/pem.h	1
verification/cbmc/include/openssl/rand.h	1
verification/cbmc/include/openssl/rsa.h	6
verification/cbmc/include/proof_allocators.h	3
verification/cbmc/include/proof_helpers/cryptosdk/make_common_data_structures.h	13
verification/cbmc/include/utils.h	5
verification/cbmc/proof_helpers.h	6
verification/cbmc/proofs/aws_cryptosdk_aes_gcm_decrypt/aws_cryptosdk_aes_gcm_decrypt_harness.c	59
verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/aws_cryptosdk_aes_gcm_encrypt_harness.c	54
verification/cbmc/proofs/aws_cryptosdk_alg_props/aws_cryptosdk_alg_props_harness.c	15
verification/cbmc/proofs/aws_cryptosdk_cmm_base_init/aws_cryptosdk_cmm_base_init_harness.c	13
verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/aws_cryptosdk_cmm_decrypt_materials_harness.c	73
verification/cbmc/proofs/aws_cryptosdk_cmm_generate_enc_materials/aws_cryptosdk_cmm_generate_enc_materials_harness.c	74
verification/cbmc/proofs/aws_cryptosdk_cmm_release/aws_cryptosdk_cmm_release_harness.c	24
verification/cbmc/proofs/aws_cryptosdk_cmm_retain/aws_cryptosdk_cmm_retain_harness.c	18
verification/cbmc/proofs/aws_cryptosdk_compare_hash_elems_by_key_string/aws_cryptosdk_compare_hash_elems_by_key_string_harness.c	39
verification/cbmc/proofs/aws_cryptosdk_dec_materials_destroy/aws_cryptosdk_dec_materials_destroy_harness.c	29
verification/cbmc/proofs/aws_cryptosdk_dec_materials_new/aws_cryptosdk_dec_materials_new_harness.c	14
verification/cbmc/proofs/aws_cryptosdk_decrypt_body/aws_cryptosdk_decrypt_body_harness.c	49
verification/cbmc/proofs/aws_cryptosdk_default_cmm_set_alg_id/aws_cryptosdk_default_cmm_set_alg_id_harness.c	18
verification/cbmc/proofs/aws_cryptosdk_deserialize_frame/aws_cryptosdk_deserialize_frame_harness.c	40
verification/cbmc/proofs/aws_cryptosdk_edk_clean_up/aws_cryptosdk_edk_clean_up_harness.c	13
verification/cbmc/proofs/aws_cryptosdk_edk_eq/aws_cryptosdk_edk_eq_harness.c	16
verification/cbmc/proofs/aws_cryptosdk_edk_init_clone/aws_cryptosdk_edk_init_clone_harness.c	20
verification/cbmc/proofs/aws_cryptosdk_edk_list_clean_up/aws_cryptosdk_edk_list_clean_up_harness.c	17
verification/cbmc/proofs/aws_cryptosdk_edk_list_clear/aws_cryptosdk_edk_list_clear_harness.c	17
verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/aws_cryptosdk_edk_list_copy_all_harness.c	89
verification/cbmc/proofs/aws_cryptosdk_edk_list_init/aws_cryptosdk_edk_list_init_harness.c	11
verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clean_up/aws_cryptosdk_enc_ctx_clean_up_harness.c	31
verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/aws_cryptosdk_enc_ctx_clear_harness.c	18
verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clone/aws_cryptosdk_enc_ctx_clone_harness.c	19
verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/aws_cryptosdk_enc_ctx_deserialize_harness.c	34
verification/cbmc/proofs/aws_cryptosdk_enc_ctx_init/aws_cryptosdk_enc_ctx_init_harness.c	7
verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/aws_cryptosdk_enc_ctx_serialize_harness.c	33
verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/aws_cryptosdk_enc_ctx_size_harness.c	36
verification/cbmc/proofs/aws_cryptosdk_enc_materials_destroy/aws_cryptosdk_enc_materials_destroy_harness.c	36
verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/aws_cryptosdk_enc_materials_new_harness.c	15
verification/cbmc/proofs/aws_cryptosdk_encrypt_body/aws_cryptosdk_encrypt_body_harness.c	49
verification/cbmc/proofs/aws_cryptosdk_genrandom/aws_cryptosdk_genrandom_harness.c	9
verification/cbmc/proofs/aws_cryptosdk_hash_elems_array_init/aws_cryptosdk_hash_elems_array_init_harness.c	22
verification/cbmc/proofs/aws_cryptosdk_hdr_size/aws_cryptosdk_hdr_size_harness.c	35
verification/cbmc/proofs/aws_cryptosdk_hdr_write/aws_cryptosdk_hdr_write_harness.c	50
verification/cbmc/proofs/aws_cryptosdk_hkdf/aws_cryptosdk_hkdf_harness.c	47
verification/cbmc/proofs/aws_cryptosdk_keyring_base_init/aws_cryptosdk_keyring_base_init_harness.c	12
verification/cbmc/proofs/aws_cryptosdk_keyring_on_decrypt/aws_cryptosdk_keyring_on_decrypt_harness.c	91
verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/aws_cryptosdk_keyring_on_encrypt_harness.c	71
verification/cbmc/proofs/aws_cryptosdk_keyring_release/aws_cryptosdk_keyring_release_harness.c	20
verification/cbmc/proofs/aws_cryptosdk_keyring_retain/aws_cryptosdk_keyring_retain_harness.c	19
verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record/aws_cryptosdk_keyring_trace_add_record_harness.c	34
verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_buf/aws_cryptosdk_keyring_trace_add_record_buf_harness.c	35
verification/cbmc/proofs/aws_cryptosdk_keyring_trace_add_record_c_str/aws_cryptosdk_keyring_trace_add_record_c_str_harness.c	32
verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clean_up/aws_cryptosdk_keyring_trace_clean_up_harness.c	15
verification/cbmc/proofs/aws_cryptosdk_keyring_trace_clear/aws_cryptosdk_keyring_trace_clear_harness.c	21
verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/aws_cryptosdk_keyring_trace_copy_all_harness.c	95
verification/cbmc/proofs/aws_cryptosdk_keyring_trace_eq/aws_cryptosdk_keyring_trace_eq_harness.c	42
verification/cbmc/proofs/aws_cryptosdk_keyring_trace_init/aws_cryptosdk_keyring_trace_init_harness.c	14
verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_clean_up/aws_cryptosdk_keyring_trace_record_clean_up_harness.c	14
verification/cbmc/proofs/aws_cryptosdk_keyring_trace_record_init_clone/aws_cryptosdk_keyring_trace_record_init_clone_harness.c	23
verification/cbmc/proofs/aws_cryptosdk_md_abort/aws_cryptosdk_md_abort_harness.c	15
verification/cbmc/proofs/aws_cryptosdk_md_finish/aws_cryptosdk_md_finish_harness.c	27
verification/cbmc/proofs/aws_cryptosdk_md_init/aws_cryptosdk_md_init_harness.c	19
verification/cbmc/proofs/aws_cryptosdk_md_size/aws_cryptosdk_md_size_harness.c	10
verification/cbmc/proofs/aws_cryptosdk_md_update/aws_cryptosdk_md_update_harness.c	28
verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/aws_cryptosdk_multi_keyring_add_child_harness.c	34
verification/cbmc/proofs/aws_cryptosdk_multi_keyring_new/MultiKeyringNew_harness.c	9
verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_decrypt/aws_cryptosdk_priv_algorithm_allowed_for_decrypt_harness.c	14
verification/cbmc/proofs/aws_cryptosdk_priv_algorithm_allowed_for_encrypt/aws_cryptosdk_priv_algorithm_allowed_for_encrypt_harness.c	10
verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_aad/aws_cryptosdk_priv_hdr_parse_aad_harness.c	43
verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_id/aws_cryptosdk_priv_hdr_parse_alg_id_harness.c	38
verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_suite_data/aws_cryptosdk_priv_hdr_parse_alg_suite_data_harness.c	35
verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_auth_tag/aws_cryptosdk_priv_hdr_parse_auth_tag_harness.c	33
verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_content_type/aws_cryptosdk_priv_hdr_parse_content_type_harness.c	38
verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_edks/aws_cryptosdk_priv_hdr_parse_edks_harness.c	55
verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_frame_len/aws_cryptosdk_priv_hdr_parse_frame_len_harness.c	37
verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_header_version/aws_cryptosdk_priv_hdr_parse_header_version_harness.c	38
verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv/aws_cryptosdk_priv_hdr_parse_iv_harness.c	33
verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_iv_len/aws_cryptosdk_priv_hdr_parse_iv_len_harness.c	38
verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_id/aws_cryptosdk_priv_hdr_parse_message_id_harness.c	34
verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_message_type/aws_cryptosdk_priv_hdr_parse_message_type_harness.c	36
verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_reserved/aws_cryptosdk_priv_hdr_parse_reserved_harness.c	36
verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c	63
verification/cbmc/proofs/aws_cryptosdk_private_algorithm_message_id_len/aws_cryptosdk_private_algorithm_message_id_len_harness.c	10
verification/cbmc/proofs/aws_cryptosdk_private_commitment_eq/aws_cryptosdk_private_commitment_eq_harness.c	28
verification/cbmc/proofs/aws_cryptosdk_private_derive_key/aws_cryptosdk_private_derive_key_harness.c	54
verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v1/aws_cryptosdk_private_derive_key_v1_harness.c	37
verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v2/aws_cryptosdk_private_derive_key_v2_harness.c	46
verification/cbmc/proofs/aws_cryptosdk_rsa_decrypt/aws_cryptosdk_rsa_decrypt_harness.c	30
verification/cbmc/proofs/aws_cryptosdk_rsa_encrypt/aws_cryptosdk_rsa_encrypt_harness.c	30
verification/cbmc/proofs/aws_cryptosdk_serialize_frame/aws_cryptosdk_serialize_frame_harness.c	28
verification/cbmc/proofs/aws_cryptosdk_session_set_commitment_policy/aws_cryptosdk_session_set_commitment_policy_harness.c	15
verification/cbmc/proofs/aws_cryptosdk_sig_abort/aws_cryptosdk_sig_abort_harness.c	29
verification/cbmc/proofs/aws_cryptosdk_sig_get_privkey/aws_cryptosdk_sig_get_privkey_harness.c	21
verification/cbmc/proofs/aws_cryptosdk_sig_get_pubkey/aws_cryptosdk_sig_get_pubkey_harness.c	25
verification/cbmc/proofs/aws_cryptosdk_sig_sign_finish/aws_cryptosdk_sig_sign_finish_harness.c	28
verification/cbmc/proofs/aws_cryptosdk_sig_sign_start/aws_cryptosdk_sig_sign_start_harness.c	26
verification/cbmc/proofs/aws_cryptosdk_sig_sign_start_keygen/aws_cryptosdk_sig_sign_start_keygen_harness.c	20
verification/cbmc/proofs/aws_cryptosdk_sig_update/aws_cryptosdk_sig_update_harness.c	25
verification/cbmc/proofs/aws_cryptosdk_sig_verify_finish/aws_cryptosdk_sig_verify_finish_harness.c	19
verification/cbmc/proofs/aws_cryptosdk_sig_verify_start/aws_cryptosdk_sig_verify_start_harness.c	21
verification/cbmc/proofs/aws_cryptosdk_sign_header/aws_cryptosdk_sign_header_harness.c	24
verification/cbmc/proofs/aws_cryptosdk_string_dup/aws_cryptosdk_string_dup_harness.c	14
verification/cbmc/proofs/aws_cryptosdk_transfer_list/aws_cryptosdk_transfer_list_harness.c	47
verification/cbmc/proofs/aws_cryptosdk_verify_header/aws_cryptosdk_verify_header_harness.c	24
verification/cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c	49
verification/cbmc/proofs/derive_data_key/derive_data_key_harness.c	55
verification/cbmc/proofs/lib/__init__.py	1
verification/cbmc/proofs/lib/print_tool_versions.py	57
verification/cbmc/proofs/lib/summarize.py	98
verification/cbmc/proofs/list_copy_all/list_copy_all_harness.c	71
verification/cbmc/proofs/run-cbmc-proofs.py	303
verification/cbmc/proofs/sign_header/sign_header_harness.c	49
verification/cbmc/sources/cbmc_invariants.c	14
verification/cbmc/sources/make_common_data_structures.c	358
verification/cbmc/sources/openssl/asn1_override.c	59
verification/cbmc/sources/openssl/bio_override.c	26
verification/cbmc/sources/openssl/bn_override.c	37
verification/cbmc/sources/openssl/ec_override.c	279
verification/cbmc/sources/openssl/err_override.c	12
verification/cbmc/sources/openssl/evp_override.c	622
verification/cbmc/sources/openssl/objects_override.c	16
verification/cbmc/sources/openssl/rand_override.c	9
verification/cbmc/sources/utils.c	28
verification/cbmc/stubs/EVP_MD_CTX_free_no_pkey_stub.c	9
verification/cbmc/stubs/EVP_PKEY_free_no_ec_key_stub.c	12
verification/cbmc/stubs/aws_add_size_checked.c	7
verification/cbmc/stubs/aws_array_list_item_generator_u8_stub.c	15
verification/cbmc/stubs/aws_array_list_sort_noop_stub.c	5
verification/cbmc/stubs/aws_atomic_fetch_add_explicit.c	6
verification/cbmc/stubs/aws_atomic_fetch_sub_explicit.c	6
verification/cbmc/stubs/aws_atomic_load_int.c	4
verification/cbmc/stubs/aws_atomic_load_ptr.c	4
verification/cbmc/stubs/aws_atomic_priv_xlate_order.c	8
verification/cbmc/stubs/aws_base64_decode.c	16
verification/cbmc/stubs/aws_base64_encode.c	22
verification/cbmc/stubs/aws_cryptosdk_enc_ctx_size_stub.c	13
verification/cbmc/stubs/aws_cryptosdk_hash_elems_array_init_stub.c	31
verification/cbmc/stubs/aws_default_allocator_stub.c	4
verification/cbmc/stubs/aws_hash_iter_overrides.c	58
verification/cbmc/stubs/evp_md_ctx_is_valid_no_pkey_stub.c	6
verification/cbmc/stubs/evp_pkey_is_valid_no_ec_key_stub.c	4
verification/cbmc/stubs/generate_enc_materials_stub.c	43
verification/cbmc/stubs/hdr_write_stub.c	20
verification/cbmc/stubs/hkdf_stub.c	17
verification/cbmc/stubs/keyring_trace_clean_up_stub.c	6
verification/cbmc/stubs/keyring_trace_clear_stub.c	7
verification/cbmc/stubs/on_encrypt_stub.c	31
verification/cbmc/stubs/transfer_list_stub.c	12