From 1384c8ef80271429c2275a62f3090c009ff41bfb Mon Sep 17 00:00:00 2001 From: Lindsay Stewart Date: Fri, 17 Jan 2025 17:44:37 -0800 Subject: [PATCH] refactor: cleanup CBMC proofs after #5048 --- crypto/s2n_evp.c | 20 -------------------- tests/cbmc/proofs/s2n_hash_free/Makefile | 1 - tests/cbmc/proofs/s2n_hash_init/Makefile | 1 - tests/cbmc/proofs/s2n_hash_new/Makefile | 1 - tests/cbmc/proofs/s2n_hmac_new/Makefile | 1 - tests/cbmc/proofs/s2n_hmac_update/Makefile | 1 - 6 files changed, 25 deletions(-) delete mode 100644 crypto/s2n_evp.c diff --git a/crypto/s2n_evp.c b/crypto/s2n_evp.c deleted file mode 100644 index d0adbb1acfc..00000000000 --- a/crypto/s2n_evp.c +++ /dev/null @@ -1,20 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * - * Licensed under the Apache License, Version 2.0 (the "License"). - * You may not use this file except in compliance with the License. - * A copy of the License is located at - * - * http://aws.amazon.com/apache2.0 - * - * or in the "license" file accompanying this file. This file is distributed - * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either - * express or implied. See the License for the specific language governing - * permissions and limitations under the License. - */ - -#include "crypto/s2n_evp.h" - -/* - * TODO: update all CBMC proofs that depend on this file, then delete. - */ diff --git a/tests/cbmc/proofs/s2n_hash_free/Makefile b/tests/cbmc/proofs/s2n_hash_free/Makefile index 5156d58ad37..676317f1dc2 100644 --- 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 index c4e7be3f29e..809625cfbdc 100644 --- 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 index 3912b92fc81..b3630936f56 100644 --- 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 index 0b293eee7d2..8a6a36b6a03 100644 --- 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 index 46efbbbb4bd..0098edb5975 100644 --- 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.