Skip to content

Commit fe97ffa

Browse files
committed
refactor: cleanup CBMC proofs after aws#5048
1 parent 9bfe1fa commit fe97ffa

File tree

13 files changed

+0
-35
lines changed

13 files changed

+0
-35
lines changed

crypto/s2n_evp.c

-20
This file was deleted.

tests/cbmc/proofs/s2n_hash_copy/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
2828
PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
2929

3030
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
31-
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
3231
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
3332
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
3433

tests/cbmc/proofs/s2n_hash_digest/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
3030
PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
3131

3232
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
33-
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
3433
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
3534

3635
# We abstract these functions because manual inspection demonstrates they are unreachable.

tests/cbmc/proofs/s2n_hash_free/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,6 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset
3636
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_init
3737
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_new
3838
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset
39-
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_allow_md5_for_fips
4039

4140
UNWINDSET +=
4241

tests/cbmc/proofs/s2n_hash_init/Makefile

-2
Original file line numberDiff line numberDiff line change
@@ -28,14 +28,12 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
2828
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
2929

3030
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
31-
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
3231

3332
# We abstract these functions because manual inspection demonstrates they are unreachable.
3433
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_copy
3534
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_new
3635
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset
3736
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_free
38-
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_allow_md5_for_fips
3937
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_copy
4038
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_free
4139
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_new

tests/cbmc/proofs/s2n_hash_new/Makefile

-2
Original file line numberDiff line numberDiff line change
@@ -25,13 +25,11 @@ PROOF_SOURCES += $(OPENSSL_SOURCE)/evp_override.c
2525
PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
2626

2727
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
28-
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
2928

3029
# We abstract these functions because manual inspection demonstrates they are unreachable.
3130
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_init
3231
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset
3332
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_free
34-
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_allow_md5_for_fips
3533
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_init
3634
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset
3735
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_free

tests/cbmc/proofs/s2n_hash_reset/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
3030
PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
3131

3232
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
33-
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
3433
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
3534

3635
# We abstract these functions because manual inspection demonstrates they are unreachable.

tests/cbmc/proofs/s2n_hash_update/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
3030
PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
3131

3232
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
33-
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
3433
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
3534

3635
# We abstract these functions because manual inspection demonstrates they are unreachable.

tests/cbmc/proofs/s2n_hmac_copy/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
2929

3030
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
3131
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hmac.c
32-
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
3332
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
3433
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
3534

tests/cbmc/proofs/s2n_hmac_init/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
3131

3232
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
3333
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hmac.c
34-
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
3534
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
3635

3736
# We abstract these functions because manual inspection demonstrates they are unreachable.

tests/cbmc/proofs/s2n_hmac_new/Makefile

-2
Original file line numberDiff line numberDiff line change
@@ -26,13 +26,11 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
2626

2727
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
2828
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hmac.c
29-
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
3029

3130
# We abstract these functions because manual inspection demonstrates they are unreachable.
3231
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_init
3332
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset
3433
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_free
35-
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_allow_md5_for_fips
3634
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_init
3735
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset
3836
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_free

tests/cbmc/proofs/s2n_hmac_reset/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
2929

3030
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
3131
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hmac.c
32-
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
3332
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
3433
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
3534

tests/cbmc/proofs/s2n_hmac_update/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
3131

3232
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hmac.c
3333
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
34-
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
3534
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
3635

3736
# We abstract these functions because manual inspection demonstrates they are unreachable.

0 commit comments

Comments
 (0)