refactor: cleanup CBMC proofs after aws#5048

lrstewart · Jan 18, 2025 · 1384c8e · 1384c8e
1 parent 9bfe1fa
commit 1384c8e
Show file tree

Hide file tree

Showing 6 changed files with 0 additions and 25 deletions.
diff --git a/crypto/s2n_evp.c b/crypto/s2n_evp.c
diff --git a/tests/cbmc/proofs/s2n_hash_free/Makefile b/tests/cbmc/proofs/s2n_hash_free/Makefile
@@ -36,7 +36,6 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_init
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_new
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_allow_md5_for_fips
 
 UNWINDSET +=
 

diff --git a/tests/cbmc/proofs/s2n_hash_init/Makefile b/tests/cbmc/proofs/s2n_hash_init/Makefile
@@ -35,7 +35,6 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_copy
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_new
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_free
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_allow_md5_for_fips
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_copy
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_free
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_new

diff --git a/tests/cbmc/proofs/s2n_hash_new/Makefile b/tests/cbmc/proofs/s2n_hash_new/Makefile
@@ -31,7 +31,6 @@ PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_init
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_free
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_allow_md5_for_fips
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_init
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_free

diff --git a/tests/cbmc/proofs/s2n_hmac_new/Makefile b/tests/cbmc/proofs/s2n_hmac_new/Makefile
@@ -32,7 +32,6 @@ PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_init
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_free
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_allow_md5_for_fips
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_init
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_free

diff --git a/tests/cbmc/proofs/s2n_hmac_update/Makefile b/tests/cbmc/proofs/s2n_hmac_update/Makefile
@@ -31,7 +31,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hmac.c
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
-PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 # We abstract these functions because manual inspection demonstrates they are unreachable.