Skip to content

Commit

Permalink
Merge branch 'main' into replace-memcmp
Browse files Browse the repository at this point in the history
  • Loading branch information
boquan-fang authored Sep 5, 2024
2 parents c541742 + 9964ee7 commit c0d426c
Show file tree
Hide file tree
Showing 163 changed files with 254 additions and 397 deletions.
79 changes: 59 additions & 20 deletions codebuild/bin/install_al2_dependencies.sh
Original file line number Diff line number Diff line change
Expand Up @@ -16,12 +16,50 @@
set -eu
source ./codebuild/bin/s2n_setup_env.sh

if [[ ${DISTRO} != "amazon linux" ]]; then
echo "Target AL2, but running on $DISTRO: Nothing to do."
exit 0
fi
al2023_main(){
case "$S2N_LIBCRYPTO" in
"openssl-3.0"|"default") echo "Installing AL2023 packages";;
*) echo "${S2N_LIBCRYPTO} is not installed on this platform."; exit 1;;
esac
common_packages
al2023_packages
versions
}

al2_main() {
echo "Installing AL2 packages"
common_packages
al2_packages
symlink_all_the_things

case "$S2N_LIBCRYPTO" in
"openssl-1.1.1")
yum erase -y openssl-devel || true
yum install -y openssl11-static openssl11-libs openssl11-devel
;;
"default") echo "Using default system libcrypto";;
*) echo "Unknown libcrypto: ${S2N_LIBCRYPTO}"; exit 1;;
esac
versions
}

common_packages(){
# Borrowed from https://github.com/aws/aws-codebuild-docker-images/blob/master/al2/x86_64/standard/5.0/Dockerfile#L24
mono
yum groupinstall -y "Development tools"
yum install -y clang git cmake3 iproute net-tools nettle-devel nettle which sudo psmisc
yum install -y python3-pip tcpdump unzip zlib-devel libtool ninja-build valgrind wget
rm /etc/yum.repos.d/mono-centos7-stable.repo
}

al2023_packages(){
# Openssl 3.0 headers and go
yum install -y openssl-devel golang
# TODO: cmake isn't finding awslc https://github.com/aws/s2n-tls/issues/4633
#./codebuild/bin/install_awslc.sh $(mktemp -d) /usr/local/awsc 0
}

base_packages() {
al2_packages() {
# Latest AL2 image had dependency issues related to NodeJS.
# We don't use NodeJS, so just remove it.
yum erase -y nodejs || true
Expand Down Expand Up @@ -52,19 +90,20 @@ symlink_all_the_things() {
update-alternatives --install /usr/bin/g++-7 g++ /usr/bin/g++ 700
}

versions(){
gcc --version
cmake --version
python3 --version
ninja --version
}

base_packages
mono
yum groupinstall -y "Development tools"
yum install -y clang cmake3 iproute net-tools nettle-devel nettle which sudo psmisc
yum install -y python3-pip tcpdump unzip zlib-devel libtool ninja-build valgrind wget
symlink_all_the_things

case "$S2N_LIBCRYPTO" in
"openssl-1.1.1")
yum erase -y openssl-devel || true
yum install -y openssl11-static openssl11-libs openssl11-devel
;;
"default") echo "Using default system libcrypto";;
*) echo "Unknown libcrypto: ${S2N_LIBCRYPTO}"; exit 1;;
esac
if [[ ${DISTRO} != "amazon linux" ]]; then
echo "Target Amazon Linux, but running on $DISTRO: Nothing to do."
exit 0;
else
if [[ ${VERSION_ID} == '2' ]]; then
al2_main;
elif [[ ${VERSION_ID} == '2023' ]]; then
al2023_main;
fi
fi
2 changes: 1 addition & 1 deletion codebuild/bin/s2n_codebuild_al2.sh
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ case "$TESTS" in
cmake . -Bbuild -DCMAKE_EXE_LINKER_FLAGS="-lcrypto -lz" -DCMAKE_EXPORT_COMPILE_COMMANDS=ON \
-DS2N_BLOCK_NONPORTABLE_OPTIMIZATIONS=True
cmake --build ./build -j $(nproc)
cmake --build ./build --target test -- ARGS="-L unit --output-on-failure"
CTEST_PARALLEL_LEVEL=$(nproc) cmake --build ./build --target test -- ARGS="-L unit --output-on-failure"
;;
*) echo "Unknown test"; exit 1;;
esac
Expand Down
2 changes: 1 addition & 1 deletion stuffer/s2n_stuffer.h
Original file line number Diff line number Diff line change
Expand Up @@ -164,7 +164,7 @@ int s2n_stuffer_copy(struct s2n_stuffer *from, struct s2n_stuffer *to, uint32_t
* "FF" == 255 or [ 0xff ]
* "0001" == 1 or [ 0x00, 0x01 ]
*/
S2N_RESULT s2n_stuffer_read_hex(struct s2n_stuffer *bytes_out, const struct s2n_blob *hex_in);
S2N_RESULT s2n_stuffer_read_hex(struct s2n_stuffer *hex_in, const struct s2n_blob *bytes_out);
S2N_RESULT s2n_stuffer_write_hex(struct s2n_stuffer *hex_out, const struct s2n_blob *bytes_in);
S2N_RESULT s2n_stuffer_read_uint8_hex(struct s2n_stuffer *stuffer, uint8_t *u);
S2N_RESULT s2n_stuffer_write_uint8_hex(struct s2n_stuffer *stuffer, uint8_t u);
Expand Down
24 changes: 11 additions & 13 deletions stuffer/s2n_stuffer_hex.c
Original file line number Diff line number Diff line change
Expand Up @@ -41,30 +41,28 @@ static S2N_RESULT s2n_stuffer_hex_digit_from_char(uint8_t c, uint8_t *i)
return S2N_RESULT_OK;
}

S2N_RESULT s2n_stuffer_read_hex(struct s2n_stuffer *bytes_out, const struct s2n_blob *hex_in)
S2N_RESULT s2n_stuffer_read_hex(struct s2n_stuffer *hex_in, const struct s2n_blob *bytes_out)
{
RESULT_PRECONDITION(s2n_stuffer_validate(bytes_out));
RESULT_PRECONDITION(s2n_blob_validate(hex_in));

size_t hex_size = hex_in->size;
size_t bytes_size = hex_in->size / 2;
RESULT_ENSURE(hex_size % 2 == 0, S2N_ERR_BAD_HEX);
if (hex_size == 0) {
RESULT_PRECONDITION(s2n_stuffer_validate(hex_in));
RESULT_PRECONDITION(s2n_blob_validate(bytes_out));
if (bytes_out->size == 0) {
return S2N_RESULT_OK;
}

RESULT_GUARD_POSIX(s2n_stuffer_reserve_space(bytes_out, bytes_size));
uint8_t *out = bytes_out->blob.data + bytes_out->write_cursor;
uint8_t *in = hex_in->data;
size_t hex_size = bytes_out->size * 2;
RESULT_ENSURE(s2n_stuffer_data_available(hex_in) >= hex_size, S2N_ERR_BAD_HEX);

for (size_t i = 0; i < bytes_size; i++) {
uint8_t *out = bytes_out->data;
uint8_t *in = hex_in->blob.data + hex_in->read_cursor;

for (size_t i = 0; i < bytes_out->size; i++) {
uint8_t hex_high = 0, hex_low = 0;
RESULT_GUARD(s2n_stuffer_hex_digit_from_char(in[(i * 2)], &hex_high));
RESULT_GUARD(s2n_stuffer_hex_digit_from_char(in[(i * 2) + 1], &hex_low));
out[i] = (hex_high * 16) + hex_low;
}

RESULT_GUARD_POSIX(s2n_stuffer_skip_write(bytes_out, bytes_size));
RESULT_GUARD_POSIX(s2n_stuffer_skip_read(hex_in, hex_size));
return S2N_RESULT_OK;
}

Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_alloc/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,6 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

# We abstract these functions because manual inspection demonstrates they are unreachable.
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_capacity/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c

PROJECT_SOURCES += $(SRCDIR)/utils/s2n_array.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

UNWINDSET +=
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_free/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,6 @@ PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_array.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

# We abstract this function because manual inspection demonstrates it is unreachable.
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_free_p/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,6 @@ PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_array.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

# We abstract this function because manual inspection demonstrates it is unreachable.
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_get/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c

PROJECT_SOURCES += $(SRCDIR)/utils/s2n_array.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

UNWINDSET +=
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_init/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,6 @@ PROOF_SOURCES += $(PROOF_STUB)/munlock.c
PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
PROOF_SOURCES += $(PROOF_STUB)/sysconf.c

PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_array.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_insert/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,6 @@ PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_array.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

# We abstract this function because manual inspection demonstrates it is unreachable.
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_insert_and_copy/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,6 @@ PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_array.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

# We abstract this function because manual inspection demonstrates it is unreachable.
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_new/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,6 @@ PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
PROOF_SOURCES += $(PROOF_STUB)/sysconf.c

PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_array.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_num_elements/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c

PROJECT_SOURCES += $(SRCDIR)/utils/s2n_array.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

UNWINDSET +=
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_pushback/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,6 @@ PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_array.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

# We abstract this function because manual inspection demonstrates it is unreachable.
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_remove/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,6 @@ PROOF_SOURCES += $(PROOF_STUB)/sysconf.c

PROJECT_SOURCES += $(SRCDIR)/utils/s2n_array.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

UNWINDSET +=
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_blob_char_to_lower/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
PROJECT_SOURCES += $(SRCDIR)/error/s2n_errno.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

# We abstract this function because manual inspection demonstrates it is unreachable.
REMOVE_FUNCTION_BODY += s2n_calculate_stacktrace
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_blob_init/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c

PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET +=

Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_blob_is_growable/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c

PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET +=

Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_blob_slice/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/error/s2n_errno.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

# We abstract this function because manual inspection demonstrates it is unreachable.
REMOVE_FUNCTION_BODY += s2n_calculate_stacktrace
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_blob_zero/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c

PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET +=

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c

PROJECT_SOURCES += $(SRCDIR)/tls/s2n_handshake_io.c
PROJECT_SOURCES += $(SRCDIR)/tls/s2n_handshake.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET +=

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_network_order.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

UNWINDSET += s2n_stuffer_write_network_order.10:9
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_network_order.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

UNWINDSET +=
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_dh_p_g_Ys_to_dh_params/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_dhe.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

UNWINDSET +=
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_dh_params_to_p_g_Ys/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_network_order.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
REMOVE_FUNCTION_BODY += s2n_free
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c

PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET +=

Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_dup/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,6 @@ PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

# We abstract these functions because manual inspection demonstrates they are unreachable.
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_free/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,6 @@ PROOF_SOURCES += $(PROOF_STUB)/sysconf.c

PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_free_object/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,6 @@ PROOF_SOURCES += $(PROOF_STUB)/sysconf.c

PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_free_or_wipe/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,6 @@ PROOF_SOURCES += $(PROOF_STUB)/sysconf.c

PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hash_allow_md5_for_fips/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c

PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

# We abstract these functions because manual inspection demonstrates they are unreachable.
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_new
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c

PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET +=

Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hash_copy/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

# We abstract these functions because manual inspection demonstrates they are unreachable.
Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hash_digest/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c

PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

# We abstract these functions because manual inspection demonstrates they are unreachable.
Expand Down
Loading

0 comments on commit c0d426c

Please sign in to comment.