Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'main' into replace-memcmp
Browse files Browse the repository at this point in the history
boquan-fang authored Sep 5, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
2 parents c541742 + 9964ee7 commit c0d426c
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
@@ -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
@@ -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
@@ -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
2 changes: 1 addition & 1 deletion stuffer/s2n_stuffer.h
Original file line number Diff line number Diff line change
@@ -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);
24 changes: 11 additions & 13 deletions stuffer/s2n_stuffer_hex.c
Original file line number Diff line number Diff line change
@@ -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;
}

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_alloc/Makefile
Original file line number Diff line number Diff line change
@@ -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
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_capacity/Makefile
Original file line number Diff line number Diff line change
@@ -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 +=
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_free/Makefile
Original file line number Diff line number Diff line change
@@ -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.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_free_p/Makefile
Original file line number Diff line number Diff line change
@@ -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.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_get/Makefile
Original file line number Diff line number Diff line change
@@ -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 +=
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_init/Makefile
Original file line number Diff line number Diff line change
@@ -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
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_insert/Makefile
Original file line number Diff line number Diff line change
@@ -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.
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
@@ -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.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_new/Makefile
Original file line number Diff line number Diff line change
@@ -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
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_num_elements/Makefile
Original file line number Diff line number Diff line change
@@ -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 +=
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_pushback/Makefile
Original file line number Diff line number Diff line change
@@ -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.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_array_remove/Makefile
Original file line number Diff line number Diff line change
@@ -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 +=
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
@@ -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
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_blob_init/Makefile
Original file line number Diff line number Diff line change
@@ -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 +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_blob_is_growable/Makefile
Original file line number Diff line number Diff line change
@@ -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 +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_blob_slice/Makefile
Original file line number Diff line number Diff line change
@@ -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
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_blob_zero/Makefile
Original file line number Diff line number Diff line change
@@ -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 +=

Original file line number Diff line number Diff line change
@@ -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 +=

Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
@@ -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 +=
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
@@ -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 +=
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
@@ -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
Original file line number Diff line number Diff line change
@@ -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 +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_dup/Makefile
Original file line number Diff line number Diff line change
@@ -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.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_free/Makefile
Original file line number Diff line number Diff line change
@@ -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
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_free_object/Makefile
Original file line number Diff line number Diff line change
@@ -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
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_free_or_wipe/Makefile
Original file line number Diff line number Diff line change
@@ -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
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
@@ -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
Original file line number Diff line number Diff line change
@@ -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 +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hash_copy/Makefile
Original file line number Diff line number Diff line change
@@ -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.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hash_digest/Makefile
Original file line number Diff line number Diff line change
@@ -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.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hash_free/Makefile
Original file line number Diff line number Diff line change
@@ -28,7 +28,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.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_evp_hash_init
Original file line number Diff line number Diff line change
@@ -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 +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hash_init/Makefile
Original file line number Diff line number Diff line change
@@ -29,7 +29,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

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_copy
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hash_is_ready_for_input/Makefile
Original file line number Diff line number Diff line change
@@ -23,7 +23,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c

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

UNWINDSET +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hash_new/Makefile
Original file line number Diff line number Diff line change
@@ -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_init
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hash_reset/Makefile
Original file line number Diff line number Diff line change
@@ -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.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hash_update/Makefile
Original file line number Diff line number Diff line change
@@ -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.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hmac_copy/Makefile
Original file line number Diff line number Diff line change
@@ -31,7 +31,6 @@ PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hmac.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.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hmac_digest/Makefile
Original file line number Diff line number Diff line change
@@ -27,7 +27,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

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

UNWINDSET +=

Original file line number Diff line number Diff line change
@@ -28,7 +28,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

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

UNWINDSET +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hmac_free/Makefile
Original file line number Diff line number Diff line change
@@ -29,7 +29,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)

PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hmac.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_evp_hash_init
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hmac_init/Makefile
Original file line number Diff line number Diff line change
@@ -33,7 +33,6 @@ PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hmac.c
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.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
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hmac_new/Makefile
Original file line number Diff line number Diff line change
@@ -27,7 +27,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hmac.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_init
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hmac_reset/Makefile
Original file line number Diff line number Diff line change
@@ -31,7 +31,6 @@ PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hmac.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.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hmac_restore_evp_hash_state/Makefile
Original file line number Diff line number Diff line change
@@ -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_hmac.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hmac_save_evp_hash_state/Makefile
Original file line number Diff line number Diff line change
@@ -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_hmac.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hmac_update/Makefile
Original file line number Diff line number Diff line change
@@ -32,7 +32,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_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

# We abstract these functions because manual inspection demonstrates they are unreachable.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_is_hello_retry_handshake/Makefile
Original file line number Diff line number Diff line change
@@ -25,7 +25,6 @@ PROJECT_SOURCES += $(SRCDIR)/tls/s2n_connection.c
PROJECT_SOURCES += $(SRCDIR)/tls/s2n_handshake_io.c
PROJECT_SOURCES += $(SRCDIR)/tls/s2n_handshake_type.c
PROJECT_SOURCES += $(SRCDIR)/tls/s2n_handshake.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_is_hello_retry_message/Makefile
Original file line number Diff line number Diff line change
@@ -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 +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_mul_overflow_harness/Makefile
Original file line number Diff line number Diff line change
@@ -20,7 +20,6 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c

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

UNWINDSET +=
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_pkcs3_to_dh_params/Makefile
Original file line number Diff line number Diff line change
@@ -34,7 +34,6 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_dhe.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
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c

Original file line number Diff line number Diff line change
@@ -35,7 +35,6 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_dhe.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
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_realloc/Makefile
Original file line number Diff line number Diff line change
@@ -32,7 +32,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

REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_set_add/Makefile
Original file line number Diff line number Diff line change
@@ -44,7 +44,6 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_array.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
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_set.c

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_set_free/Makefile
Original file line number Diff line number Diff line change
@@ -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
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_set.c

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_set_free_p/Makefile
Original file line number Diff line number Diff line change
@@ -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
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_set.c

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_set_get/Makefile
Original file line number Diff line number Diff line change
@@ -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
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_set.c

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_set_len/Makefile
Original file line number Diff line number Diff line change
@@ -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
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_set.c

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_set_new/Makefile
Original file line number Diff line number Diff line change
@@ -32,7 +32,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
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_set_remove/Makefile
Original file line number Diff line number Diff line change
@@ -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
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_set.c

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_socket_write/Makefile
Original file line number Diff line number Diff line change
@@ -18,7 +18,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
PROOF_SOURCES += $(PROOF_STUB)/write.c

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

include ../Makefile.common
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_socket_write_cork/Makefile
Original file line number Diff line number Diff line change
@@ -18,7 +18,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROOF_SOURCES += $(PROOF_STUB)/setsockopt.c
PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c

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

include ../Makefile.common
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_socket_write_restore/Makefile
Original file line number Diff line number Diff line change
@@ -18,7 +18,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROOF_SOURCES += $(PROOF_STUB)/setsockopt.c
PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c

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

include ../Makefile.common
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_socket_write_snapshot/Makefile
Original file line number Diff line number Diff line change
@@ -18,7 +18,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROOF_SOURCES += $(PROOF_STUB)/getsockopt.c
PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c

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

include ../Makefile.common
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_socket_write_uncork/Makefile
Original file line number Diff line number Diff line change
@@ -18,7 +18,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROOF_SOURCES += $(PROOF_STUB)/setsockopt.c
PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c

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

include ../Makefile.common
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_alloc/Makefile
Original file line number Diff line number Diff line change
@@ -35,7 +35,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.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.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_fd/Makefile
Original file line number Diff line number Diff line change
@@ -29,7 +29,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_file.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_file/Makefile
Original file line number Diff line number Diff line change
@@ -33,7 +33,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_file.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET += s2n_stuffer_alloc_ro_from_file.6:3

Original file line number Diff line number Diff line change
@@ -32,7 +32,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_text.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.
Original file line number Diff line number Diff line change
@@ -39,7 +39,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

# We abstract this function because manual inspection demonstrates it is unreachable.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_copy/Makefile
Original file line number Diff line number Diff line change
@@ -33,7 +33,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.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 this function because manual inspection demonstrates it is unreachable.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_dhparams_from_pem/Makefile
Original file line number Diff line number Diff line change
@@ -39,7 +39,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

# We abstract these functions because manual inspection demonstrates they are unreachable.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_erase_and_read/Makefile
Original file line number Diff line number Diff line change
@@ -27,7 +27,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

#No loops to unwind
UNWINDSET +=
Original file line number Diff line number Diff line change
@@ -26,7 +26,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

#No loops to unwind
UNWINDSET +=
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_extract_blob/Makefile
Original file line number Diff line number Diff line change
@@ -32,7 +32,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.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 this function because manual inspection demonstrates it is unreachable.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_free/Makefile
Original file line number Diff line number Diff line change
@@ -30,7 +30,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.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.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_get_vector_size/Makefile
Original file line number Diff line number Diff line change
@@ -29,6 +29,5 @@ 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

include ../Makefile.common
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_growable_alloc/Makefile
Original file line number Diff line number Diff line change
@@ -33,7 +33,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.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.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_init/Makefile
Original file line number Diff line number Diff line change
@@ -25,7 +25,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

#No loops to unwind
UNWINDSET +=
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_is_consumed/Makefile
Original file line number Diff line number Diff line change
@@ -26,7 +26,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROJECT_SOURCES += $(SRCDIR)/error/s2n_errno.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.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
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_peek_char/Makefile
Original file line number Diff line number Diff line change
@@ -28,7 +28,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_network_order.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_text.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_peek_check_for_str/Makefile
Original file line number Diff line number Diff line change
@@ -31,7 +31,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_network_order.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_text.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET += strlen.0:$(call addone,$(MAX_STRING_LEN))
UNWINDSET += memcmp.0:$(call addone,$(MAX_STRING_LEN))
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_printf/Makefile
Original file line number Diff line number Diff line change
@@ -33,6 +33,5 @@ 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

include ../Makefile.common
Original file line number Diff line number Diff line change
@@ -41,7 +41,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 this function because manual inspection demonstrates it is unreachable.
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_raw_read/Makefile
Original file line number Diff line number Diff line change
@@ -26,7 +26,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

#No loops to unwind
UNWINDSET +=
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_raw_write/Makefile
Original file line number Diff line number Diff line change
@@ -30,7 +30,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.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.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_read/Makefile
Original file line number Diff line number Diff line change
@@ -26,7 +26,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

#No loops to unwind
UNWINDSET +=
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_read_base64/Makefile
Original file line number Diff line number Diff line change
@@ -36,7 +36,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_base64.c
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_result.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_read_bytes/Makefile
Original file line number Diff line number Diff line change
@@ -27,7 +27,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

#No loops to unwind
UNWINDSET +=
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_read_expected_str/Makefile
Original file line number Diff line number Diff line change
@@ -29,7 +29,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_network_order.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_text.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET += strlen.0:$(call addone,$(MAX_STRING_LEN))
UNWINDSET += memcmp.0:$(call addone,$(MAX_STRING_LEN))
3 changes: 1 addition & 2 deletions tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile
Original file line number Diff line number Diff line change
@@ -35,9 +35,8 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.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_read_hex.8:$(MAX_BLOB_SIZE)
UNWINDSET += s2n_stuffer_read_hex.7:$(MAX_BLOB_SIZE)

include ../Makefile.common
Original file line number Diff line number Diff line change
@@ -24,42 +24,29 @@ void s2n_stuffer_read_hex_harness()
{
nondet_s2n_mem_init();

struct s2n_stuffer *output = cbmc_allocate_s2n_stuffer();
__CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(output)));
struct s2n_stuffer *input = cbmc_allocate_s2n_stuffer();
__CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(input)));

struct s2n_blob *hex_in = cbmc_allocate_s2n_blob();
__CPROVER_assume(s2n_result_is_ok(s2n_blob_validate(hex_in)));
__CPROVER_assume(s2n_blob_is_bounded(hex_in, MAX_BLOB_SIZE));
struct s2n_blob *output = cbmc_allocate_s2n_blob();
__CPROVER_assume(s2n_result_is_ok(s2n_blob_validate(output)));
__CPROVER_assume(s2n_blob_is_bounded(output, MAX_BLOB_SIZE - 1));

struct s2n_stuffer old_output = *output;
struct store_byte_from_buffer output_saved_byte = { 0 };
save_byte_from_blob(&output->blob, &output_saved_byte);
__CPROVER_assume(output_saved_byte.idx < output->write_cursor);
struct s2n_stuffer old_input = *input;
struct s2n_blob old_output = *output;
struct store_byte_from_buffer input_saved_byte = { 0 };
save_byte_from_blob(&input->blob, &input_saved_byte);

struct s2n_blob old_hex_in = *hex_in;
struct store_byte_from_buffer old_hex_in_byte = { 0 };
save_byte_from_blob(hex_in, &old_hex_in_byte);
s2n_result result = s2n_stuffer_read_hex(input, output);

s2n_result result = s2n_stuffer_read_hex(output, hex_in);

struct s2n_stuffer expected_bytes_out = old_output;
struct s2n_blob expected_hex_in = old_hex_in;

/* On success, the byte equivalent of the hex was written to the stuffer */
/* On success, enough hex to fill the blob was read from the stuffer */
struct s2n_stuffer expected_input = old_input;
if (s2n_result_is_ok(result)) {
expected_bytes_out.write_cursor += old_hex_in.size / 2;
expected_bytes_out.high_water_mark = MAX(expected_bytes_out.write_cursor,
old_output.high_water_mark);
}

/* Memory may be allocated on either success or failure,
* because we allocated the memory before we start writing. */
if (output->blob.size > old_output.blob.size) {
expected_bytes_out.blob = output->blob;
expected_input.read_cursor += old_output.size * 2;
}
assert(s2n_result_is_ok(s2n_stuffer_validate(input)));
assert_stuffer_equivalence(input, &expected_input, &input_saved_byte);

assert(s2n_result_is_ok(s2n_stuffer_validate(output)));
assert_stuffer_equivalence(output, &expected_bytes_out, &output_saved_byte);
assert(s2n_result_is_ok(s2n_blob_validate(hex_in)));
assert_blob_equivalence(hex_in, &expected_hex_in, &old_hex_in_byte);
/* Only the data in the blob changes, so check equivalent without a saved byte */
assert(s2n_result_is_ok(s2n_blob_validate(output)));
assert_blob_equivalence(output, &old_output, NULL);
}
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_read_line/Makefile
Original file line number Diff line number Diff line change
@@ -37,7 +37,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
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_read_token/Makefile
Original file line number Diff line number Diff line change
@@ -36,7 +36,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 += s2n_blob_slice
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_read_uint16/Makefile
Original file line number Diff line number Diff line change
@@ -26,7 +26,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_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/Makefile
Original file line number Diff line number Diff line change
@@ -29,7 +29,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.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

REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_read_uint24/Makefile
Original file line number Diff line number Diff line change
@@ -26,7 +26,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_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_read_uint32/Makefile
Original file line number Diff line number Diff line change
@@ -26,7 +26,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_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_read_uint64/Makefile
Original file line number Diff line number Diff line change
@@ -26,7 +26,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_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_read_uint8/Makefile
Original file line number Diff line number Diff line change
@@ -26,7 +26,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_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/Makefile
Original file line number Diff line number Diff line change
@@ -29,7 +29,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.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

REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_recv_from_fd/Makefile
Original file line number Diff line number Diff line change
@@ -37,7 +37,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
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_reread/Makefile
Original file line number Diff line number Diff line change
@@ -26,7 +26,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

#No loops to unwind
UNWINDSET +=
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_reserve/Makefile
Original file line number Diff line number Diff line change
@@ -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
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_reserve_space/Makefile
Original file line number Diff line number Diff line change
@@ -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 += s2n_blob_slice
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_reserve_uint16/Makefile
Original file line number Diff line number Diff line change
@@ -34,7 +34,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 += s2n_blob_slice
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_reserve_uint24/Makefile
Original file line number Diff line number Diff line change
@@ -34,7 +34,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 += s2n_blob_slice
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_resize/Makefile
Original file line number Diff line number Diff line change
@@ -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
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_resize_if_empty/Makefile
Original file line number Diff line number Diff line change
@@ -31,7 +31,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.
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_rewind_read/Makefile
Original file line number Diff line number Diff line change
@@ -25,7 +25,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c

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

UNWINDSET +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_rewrite/Makefile
Original file line number Diff line number Diff line change
@@ -25,7 +25,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c

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

UNWINDSET +=

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_send_to_fd/Makefile
Original file line number Diff line number Diff line change
@@ -33,7 +33,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

REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_shift/Makefile
Original file line number Diff line number Diff line change
@@ -32,7 +32,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.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 += memmove_impl.0:$(call addone,$(MAX_BLOB_SIZE))
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_skip_expected_char/Makefile
Original file line number Diff line number Diff line change
@@ -28,7 +28,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_text.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET += s2n_stuffer_skip_expected_char.4:$(call addone,$(MAX_BLOB_SIZE))

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_skip_read/Makefile
Original file line number Diff line number Diff line change
@@ -26,7 +26,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

#No loops to unwind
UNWINDSET +=
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_skip_read_until/Makefile
Original file line number Diff line number Diff line change
@@ -35,7 +35,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_network_order.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_text.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET += s2n_stuffer_skip_read_until.10:$(call addone,$(MAX_BLOB_SIZE))
UNWINDSET += s2n_stuffer_skip_to_char.1:$(call addone,$(MAX_BLOB_SIZE))
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_skip_to_char/Makefile
Original file line number Diff line number Diff line change
@@ -28,7 +28,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_text.c
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_result.c

UNWINDSET += s2n_stuffer_skip_to_char.1:$(call addone,$(MAX_BLOB_SIZE))

1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_skip_whitespace/Makefile
Original file line number Diff line number Diff line change
@@ -28,7 +28,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_text.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

UNWINDSET += s2n_stuffer_skip_whitespace.0:$(call addone,$(MAX_BLOB_SIZE))
UNWINDSET += s2n_stuffer_skip_whitespace.1:$(call addone,$(MAX_BLOB_SIZE))
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_skip_write/Makefile
Original file line number Diff line number Diff line change
@@ -34,7 +34,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
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_wipe/Makefile
Original file line number Diff line number Diff line change
@@ -25,7 +25,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

#No loops to unwind
UNWINDSET +=
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_wipe_n/Makefile
Original file line number Diff line number Diff line change
@@ -26,7 +26,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c

#No loops to unwind
UNWINDSET +=
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_write/Makefile
Original file line number Diff line number Diff line change
@@ -31,7 +31,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 += s2n_blob_slice
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_write_base64/Makefile
Original file line number Diff line number Diff line change
@@ -38,7 +38,6 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.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
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_write_bytes/Makefile
Original file line number Diff line number Diff line change
@@ -31,7 +31,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 += s2n_blob_slice
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile
Original file line number Diff line number Diff line change
@@ -35,7 +35,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.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_hex.3:$(call addone,$(MAX_BLOB_SIZE))
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_write_network_order/Makefile
Original file line number Diff line number Diff line change
@@ -33,7 +33,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
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_write_reservation/Makefile
Original file line number Diff line number Diff line change
@@ -40,7 +40,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 += s2n_blob_slice
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_write_uint16/Makefile
Original file line number Diff line number Diff line change
@@ -33,7 +33,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 += s2n_blob_slice
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile
Original file line number Diff line number Diff line change
@@ -32,7 +32,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.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 += __CPROVER_file_local_s2n_stuffer_hex_c_s2n_stuffer_hex_write_n_bytes.4:5
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_write_uint24/Makefile
Original file line number Diff line number Diff line change
@@ -33,7 +33,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 += s2n_blob_slice
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_write_uint32/Makefile
Original file line number Diff line number Diff line change
@@ -33,7 +33,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 += s2n_blob_slice
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_write_uint64/Makefile
Original file line number Diff line number Diff line change
@@ -33,7 +33,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 += s2n_blob_slice
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_write_uint8/Makefile
Original file line number Diff line number Diff line change
@@ -32,7 +32,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 += s2n_blob_slice
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile
Original file line number Diff line number Diff line change
@@ -32,7 +32,6 @@ PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.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 += __CPROVER_file_local_s2n_stuffer_hex_c_s2n_stuffer_hex_write_n_bytes.4:3
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_write_vector_size/Makefile
Original file line number Diff line number Diff line change
@@ -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 += s2n_add_overflow
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_stuffer_writev_bytes/Makefile
Original file line number Diff line number Diff line change
@@ -38,7 +38,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 += s2n_blob_slice
2 changes: 1 addition & 1 deletion tests/pcap/Cargo.toml
Original file line number Diff line number Diff line change
@@ -6,14 +6,14 @@ publish = false

[features]
default = []
ja4 = [] # Older versions of tshark do not support JA4
download = [] # Download additional pcaps from a list of configured urls

[build-dependencies]
anyhow = "1.0.86"
bytes = "1.7.1"
hex = "0.4.3"
reqwest = { version = "0.12.7", features = ["blocking"] }
semver = "1.0.23"

[dependencies]
anyhow = "1.0.86"
35 changes: 35 additions & 0 deletions tests/pcap/build.rs
Original file line number Diff line number Diff line change
@@ -4,10 +4,12 @@
use anyhow::*;
use bytes::Buf;
use bytes::Bytes;
use semver::Version;
use std::collections::HashMap;
use std::fs::File;
use std::io::copy;
use std::path::Path;
use std::process::Command;
use std::thread;
use std::time::Duration;

@@ -101,7 +103,40 @@ fn download(url: &str) -> Result<Bytes> {
bail!("Unable to download: {}", url);
}

fn assert_tshark_version() -> Result<()> {
let output = Command::new("tshark").args(["--version"]).output();
let version = output.ok().and_then(|output| {
let message = std::str::from_utf8(&output.stdout).ok();
message.and_then(|msg| msg.split_whitespace().find_map(|s| Version::parse(s).ok()))
});

// Version requirements:
// 1. tshark >= 3.7.0 is required for JA3 support
// JA3 support was added to earlier versions, but did not correctly ignore grease values.
// See https://gitlab.com/wireshark/wireshark/-/commit/03afef0a566ed649ead587fb4c02fc2d8539f3b7
// 2. tshark >= 4.1.0 is required for consistent handling of sslv2.
// Otherwise, we have to branch on sslv2 message filters.
// See https://gitlab.com/wireshark/wireshark/-/commit/aee0278e086469a4b5b3185947a95556fd3ae708
// 3. tshark >= 4.2.0 is required for JA4 support.
// See https://gitlab.com/wireshark/wireshark/-/commit/fd19f0d06f96b9934e3cd5b9889b2f83d3567fce
let min_version = Version::new(4, 2, 0);
if let Some(version) = version {
assert!(
version >= min_version,
"tshark {} required. tshark {} found",
min_version,
version
);
println!("tshark version: {}", version);
} else {
println!("cargo:warning=Unable to determine tshark version");
}
Ok(())
}

fn main() -> Result<()> {
assert_tshark_version()?;

let out_dir = std::env::var("OUT_DIR")?;
let download_path = Path::new(&out_dir).join("downloaded_pcaps");

2 changes: 2 additions & 0 deletions tests/pcap/src/handshake_message.rs
Original file line number Diff line number Diff line change
@@ -138,6 +138,8 @@ impl Builder {
const TCP_PAYLOAD: &'static str = "tcp.payload";
const TCP_REASSEMBLED: &'static str = "tcp.reassembled.data";

// Note: sslv2 uses "tls.ssl2.handshake.type" instead. If we want to support
// sslv2 ClientHellos, we will need to search for both variants.
const MESSAGE_TYPE: &'static str = "tls.handshake.type";

pub(crate) fn set_type(&mut self, message_type: u8) -> &mut Self {
4 changes: 1 addition & 3 deletions tests/pcap/tests/s2n_client_hellos.rs
Original file line number Diff line number Diff line change
@@ -6,6 +6,7 @@ use pcap::all_pcaps;
use pcap::client_hello::ClientHello as PcapHello;
use pcap::handshake_message::Builder;
use s2n_tls::client_hello::{ClientHello as S2NHello, FingerprintType};
use s2n_tls::fingerprint;

fn get_s2n_hello(pcap_hello: &PcapHello) -> Result<Box<S2NHello>> {
let bytes = pcap_hello.message().bytes();
@@ -63,11 +64,8 @@ fn ja3_fingerprints() -> Result<()> {
})
}

#[cfg(feature = "ja4")]
#[test]
fn ja4_fingerprints() -> Result<()> {
use s2n_tls::fingerprint;

let mut builder = fingerprint::Builder::new(FingerprintType::JA4)?;

test_all_client_hellos(|pcap_hello, s2n_hello| {
1 change: 0 additions & 1 deletion tests/sidetrail/working/s2n-cbc/Makefile
Original file line number Diff line number Diff line change
@@ -13,7 +13,6 @@ extras += crypto/s2n_hmac.c
extras += error/s2n_errno.c
extras += tls/s2n_cbc.c
extras += utils/s2n_ensure.c
extras += utils/s2n_result.c
extras += utils/s2n_safety.c
goals += simple_cbc_wrapper@cbc.c
full_self_comp += true
1 change: 0 additions & 1 deletion tests/sidetrail/working/s2n-cbc/copy_as_needed.sh
Original file line number Diff line number Diff line change
@@ -41,7 +41,6 @@ cp $S2N_BASE/tls/s2n_cbc.c tls/
patch -p5 < ../patches/cbc.patch

mkdir -p utils
cp $S2N_BASE/utils/s2n_result.c utils/
cp $S2N_BASE/utils/s2n_safety.c utils/
patch -p1 < ../patches/safety.patch

1 change: 0 additions & 1 deletion tests/sidetrail/working/s2n-record-read-aead/Makefile
Original file line number Diff line number Diff line change
@@ -19,7 +19,6 @@ extras += tls/s2n_record_read_aead.c
extras += utils/s2n_blob.c
extras += utils/s2n_ensure.c
extras += utils/s2n_mem.c
extras += utils/s2n_result.c
extras += utils/s2n_safety.c
goals += s2n_record_parse_wrapper@s2n_record_read_wrapper.c
#goals += test_leakage@s2n_record_read_wrapper.c
Original file line number Diff line number Diff line change
@@ -47,7 +47,6 @@ patch -p5 < ../patches/cbc.patch

mkdir -p utils
cp $S2N_BASE/utils/s2n_blob.c utils/
cp $S2N_BASE/utils/s2n_result.c utils/
cp $S2N_BASE/utils/s2n_result.h utils/
cp $S2N_BASE/utils/s2n_safety.c utils/
cp $S2N_BASE/utils/s2n_safety.h utils/
Original file line number Diff line number Diff line change
@@ -17,7 +17,6 @@ extras += tls/s2n_cbc.c
extras += tls/s2n_record_read_cbc.c
extras += utils/s2n_ensure.c
extras += utils/s2n_mem.c
extras += utils/s2n_result.c
extras += utils/s2n_safety.c
goals += s2n_record_parse_wrapper@s2n_record_read_wrapper.c
#goals += test_leakage@s2n_record_read_wrapper.c
Original file line number Diff line number Diff line change
@@ -46,7 +46,6 @@ cp $S2N_BASE/tls/s2n_record_read_cbc.c tls/
patch -p1 < record_read_cbc.patch

mkdir -p utils
cp $S2N_BASE/utils/s2n_result.c utils/
cp $S2N_BASE/utils/s2n_safety.c utils/
patch -p1 < ../patches/safety.patch

1 change: 0 additions & 1 deletion tests/sidetrail/working/s2n-record-read-cbc/Makefile
Original file line number Diff line number Diff line change
@@ -17,7 +17,6 @@ extras += tls/s2n_cbc.c
extras += tls/s2n_record_read_cbc.c
extras += utils/s2n_ensure.c
extras += utils/s2n_mem.c
extras += utils/s2n_result.c
extras += utils/s2n_safety.c
goals += s2n_record_parse_wrapper@s2n_record_read_wrapper.c
#goals += test_leakage@s2n_record_read_wrapper.c
Original file line number Diff line number Diff line change
@@ -46,7 +46,6 @@ cp $S2N_BASE/tls/s2n_record_read_cbc.c tls/
patch -p1 < record_read_cbc.patch

mkdir -p utils
cp $S2N_BASE/utils/s2n_result.c utils/
cp $S2N_BASE/utils/s2n_safety.c utils/
patch -p1 < ../patches/safety.patch

1 change: 0 additions & 1 deletion tests/sidetrail/working/s2n-record-read-composite/Makefile
Original file line number Diff line number Diff line change
@@ -16,7 +16,6 @@ extras += stuffer/s2n_stuffer_network_order.c
extras += tls/s2n_record_read_composite.c
extras += utils/s2n_ensure.c
extras += utils/s2n_mem.c
extras += utils/s2n_result.c
extras += utils/s2n_safety.c
goals += s2n_record_parse_wrapper@s2n_record_read_wrapper.c
#goals += test_leakage@s2n_record_read_wrapper.c
Original file line number Diff line number Diff line change
@@ -47,7 +47,6 @@ patch -p5 < ../patches/cbc.patch
patch -p1 < record_read.patch

mkdir -p utils
cp $S2N_BASE/utils/s2n_result.c utils/
cp $S2N_BASE/utils/s2n_safety.c utils/
patch -p1 < ../patches/safety.patch

1 change: 0 additions & 1 deletion tests/sidetrail/working/s2n-record-read-stream/Makefile
Original file line number Diff line number Diff line change
@@ -17,7 +17,6 @@ extras += tls/s2n_cbc.c
extras += tls/s2n_record_read_stream.c
extras += utils/s2n_ensure.c
extras += utils/s2n_mem.c
extras += utils/s2n_result.c
extras += utils/s2n_safety.c
goals += s2n_record_parse_wrapper@s2n_record_read_wrapper.c
full_self_comp += true
Original file line number Diff line number Diff line change
@@ -46,7 +46,6 @@ cp $S2N_BASE/tls/s2n_record_read_stream.c tls/
patch -p1 < s2n_record_read_stream.patch

mkdir -p utils
cp $S2N_BASE/utils/s2n_result.c utils/
cp $S2N_BASE/utils/s2n_safety.c utils/
patch -p1 < ../patches/safety.patch

28 changes: 12 additions & 16 deletions tests/testlib/s2n_hex_testlib.c
Original file line number Diff line number Diff line change
@@ -25,15 +25,18 @@ S2N_RESULT s2n_stuffer_alloc_from_hex(struct s2n_stuffer *bytes_out, const char
RESULT_ENSURE_REF(bytes_out);
RESULT_ENSURE_REF(hex_cstr);

DEFER_CLEANUP(struct s2n_blob hex = { 0 }, s2n_free);
DEFER_CLEANUP(struct s2n_stuffer hex = { 0 }, s2n_stuffer_free);
/* Copying the hex into heap memory to handle the 'const' isn't exactly efficient,
* but for a testlib method it is sufficient.
*/
RESULT_GUARD_POSIX(s2n_alloc(&hex, strlen(hex_cstr)));
RESULT_CHECKED_MEMCPY(hex.data, hex_cstr, hex.size);

RESULT_GUARD_POSIX(s2n_stuffer_alloc(bytes_out, strlen(hex_cstr) / 2));
RESULT_GUARD(s2n_stuffer_read_hex(bytes_out, &hex));
RESULT_GUARD_POSIX(s2n_stuffer_alloc(&hex, strlen(hex_cstr)));
RESULT_GUARD_POSIX(s2n_stuffer_write_str(&hex, hex_cstr));

uint32_t bytes_size = strlen(hex_cstr) / 2;
RESULT_GUARD_POSIX(s2n_stuffer_alloc(bytes_out, bytes_size));
RESULT_GUARD(s2n_stuffer_read_hex(&hex, &bytes_out->blob));
RESULT_ENSURE(s2n_stuffer_data_available(&hex) == 0, S2N_ERR_BAD_HEX);
RESULT_GUARD_POSIX(s2n_stuffer_skip_write(bytes_out, bytes_size));
return S2N_RESULT_OK;
}

@@ -51,16 +54,9 @@ S2N_RESULT s2n_blob_alloc_from_hex_with_whitespace(struct s2n_blob *bytes_out, c
RESULT_GUARD_POSIX(s2n_stuffer_write_uint8(&hex_in, hex_cstr[i]));
}
uint32_t hex_in_size = s2n_stuffer_data_available(&hex_in);
hex_in.blob.size = hex_in_size;

DEFER_CLEANUP(struct s2n_blob bytes_out_mem = { 0 }, s2n_free);
RESULT_GUARD_POSIX(s2n_alloc(&bytes_out_mem, hex_in_size / 2));

struct s2n_stuffer bytes_out_stuffer = { 0 };
RESULT_GUARD_POSIX(s2n_stuffer_init(&bytes_out_stuffer, &bytes_out_mem));
RESULT_GUARD(s2n_stuffer_read_hex(&bytes_out_stuffer, &hex_in.blob));

*bytes_out = bytes_out_mem;
ZERO_TO_DISABLE_DEFER_CLEANUP(bytes_out_mem);
RESULT_GUARD_POSIX(s2n_alloc(bytes_out, hex_in_size / 2));
RESULT_GUARD(s2n_stuffer_read_hex(&hex_in, bytes_out));
RESULT_ENSURE(s2n_stuffer_data_available(&hex_in) == 0, S2N_ERR_BAD_HEX);
return S2N_RESULT_OK;
}
14 changes: 4 additions & 10 deletions tests/unit/s2n_self_talk_key_log_test.c
Original file line number Diff line number Diff line change
@@ -180,16 +180,10 @@ int main(int argc, char **argv)
EXPECT_SUCCESS(s2n_blob_init(&raw_bytes, bytes, sizeof(bytes)));
EXPECT_OK(s2n_stuffer_write_hex(&encoded, &raw_bytes));

DEFER_CLEANUP(struct s2n_stuffer decoded, s2n_stuffer_free);
EXPECT_SUCCESS(s2n_stuffer_alloc(&decoded, sizeof(bytes)));

encoded.blob.size = s2n_stuffer_data_available(&encoded);
EXPECT_OK(s2n_stuffer_read_hex(&decoded, &encoded.blob));

uint8_t *out = s2n_stuffer_raw_read(&decoded, s2n_stuffer_data_available(&decoded));
EXPECT_NOT_NULL(out);

EXPECT_EQUAL(memcmp(bytes, out, sizeof(bytes)), 0);
DEFER_CLEANUP(struct s2n_blob decoded = { 0 }, s2n_free);
EXPECT_SUCCESS(s2n_alloc(&decoded, sizeof(bytes)));
EXPECT_OK(s2n_stuffer_read_hex(&encoded, &decoded));
EXPECT_BYTEARRAY_EQUAL(decoded.data, bytes, sizeof(bytes));
};

END_TEST();
68 changes: 26 additions & 42 deletions tests/unit/s2n_stuffer_hex_test.c
Original file line number Diff line number Diff line change
@@ -135,14 +135,12 @@ int main(int argc, char **argv)
EXPECT_SUCCESS(s2n_stuffer_alloc(&hex_in, expected_size));
EXPECT_SUCCESS(s2n_stuffer_write_text(&hex_in, test_cases[i].hex, expected_size));

DEFER_CLEANUP(struct s2n_stuffer num_out = { 0 }, s2n_stuffer_free);
EXPECT_SUCCESS(s2n_stuffer_growable_alloc(&num_out, 0));
EXPECT_OK(s2n_stuffer_read_hex(&num_out, &hex_in.blob));

uint8_t actual_num = 0;
EXPECT_SUCCESS(s2n_stuffer_read_uint8(&num_out, &actual_num));
struct s2n_blob num_out = { 0 };
EXPECT_SUCCESS(s2n_blob_init(&num_out, &actual_num, 1));
EXPECT_OK(s2n_stuffer_read_hex(&hex_in, &num_out));
EXPECT_EQUAL(actual_num, test_cases[i].num);
EXPECT_FALSE(s2n_stuffer_data_available(&num_out));
EXPECT_FALSE(s2n_stuffer_data_available(&hex_in));
};
}
};
@@ -237,8 +235,10 @@ int main(int argc, char **argv)
EXPECT_SUCCESS(s2n_stuffer_write_text(&hex_in, test_cases[i].hex, expected_size));

DEFER_CLEANUP(struct s2n_stuffer num_out = { 0 }, s2n_stuffer_free);
EXPECT_SUCCESS(s2n_stuffer_growable_alloc(&num_out, 0));
EXPECT_OK(s2n_stuffer_read_hex(&num_out, &hex_in.blob));
EXPECT_SUCCESS(s2n_stuffer_alloc(&num_out, sizeof(uint16_t)));
EXPECT_OK(s2n_stuffer_read_hex(&hex_in, &num_out.blob));
EXPECT_SUCCESS(s2n_stuffer_skip_write(&num_out, num_out.blob.size));
EXPECT_FALSE(s2n_stuffer_data_available(&hex_in));

uint16_t actual_num = 0;
EXPECT_SUCCESS(s2n_stuffer_read_uint16(&num_out, &actual_num));
@@ -332,15 +332,11 @@ int main(int argc, char **argv)
EXPECT_SUCCESS(s2n_stuffer_alloc(&hex_in, hex_size));
EXPECT_SUCCESS(s2n_stuffer_write_text(&hex_in, test_cases[i].hex, hex_size));

DEFER_CLEANUP(struct s2n_stuffer num_out = { 0 }, s2n_stuffer_free);
EXPECT_SUCCESS(s2n_stuffer_growable_alloc(&num_out, 0));
EXPECT_OK(s2n_stuffer_read_hex(&num_out, &hex_in.blob));

size_t actual_size = s2n_stuffer_data_available(&num_out);
EXPECT_EQUAL(actual_size, test_cases[i].bytes_size);

const uint8_t *actual_bytes = s2n_stuffer_raw_read(&num_out, actual_size);
EXPECT_BYTEARRAY_EQUAL(actual_bytes, test_cases[i].bytes, actual_size);
DEFER_CLEANUP(struct s2n_blob num_out = { 0 }, s2n_free);
EXPECT_SUCCESS(s2n_alloc(&num_out, test_cases[i].bytes_size));
EXPECT_OK(s2n_stuffer_read_hex(&hex_in, &num_out));
EXPECT_BYTEARRAY_EQUAL(num_out.data, test_cases[i].bytes, test_cases[i].bytes_size);
EXPECT_FALSE(s2n_stuffer_data_available(&hex_in));
};
}
};
@@ -393,17 +389,13 @@ int main(int argc, char **argv)
EXPECT_SUCCESS(s2n_stuffer_alloc(&hex, strlen(test_hex)));
EXPECT_SUCCESS(s2n_stuffer_write_str(&hex, test_hex));

DEFER_CLEANUP(struct s2n_stuffer out = { 0 }, s2n_stuffer_free);
EXPECT_SUCCESS(s2n_stuffer_growable_alloc(&out, 0));
DEFER_CLEANUP(struct s2n_blob out = { 0 }, s2n_free);
EXPECT_SUCCESS(s2n_alloc(&out, sizeof(uint8_t)));
if (i == 0) {
EXPECT_OK(s2n_stuffer_read_hex(&out, &hex.blob));
} else if (strlen(test_hex) == 0) {
/* Unlike s2n_stuffer_read_uint8_hex, read_hex accepts
* empty input since it has no size expectations */
EXPECT_OK(s2n_stuffer_read_hex(&out, &hex.blob));
EXPECT_OK(s2n_stuffer_read_hex(&hex, &out));
} else {
EXPECT_ERROR_WITH_ERRNO(
s2n_stuffer_read_hex(&out, &hex.blob),
s2n_stuffer_read_hex(&hex, &out),
S2N_ERR_BAD_HEX);
}
};
@@ -456,18 +448,13 @@ int main(int argc, char **argv)
EXPECT_SUCCESS(s2n_stuffer_alloc(&hex, strlen(test_hex)));
EXPECT_SUCCESS(s2n_stuffer_write_str(&hex, test_hex));

DEFER_CLEANUP(struct s2n_stuffer out = { 0 }, s2n_stuffer_free);
EXPECT_SUCCESS(s2n_stuffer_growable_alloc(&out, 0));
DEFER_CLEANUP(struct s2n_blob out = { 0 }, s2n_free);
EXPECT_SUCCESS(s2n_alloc(&out, sizeof(uint16_t)));
if (i == 0) {
EXPECT_OK(s2n_stuffer_read_hex(&out, &hex.blob));
} else if (strlen(test_hex) < sizeof(uint16_t) * 2
&& strlen(test_hex) % 2 == 0) {
/* Unlike s2n_stuffer_read_uint16_hex, read_hex accepts
* input of any valid size */
EXPECT_OK(s2n_stuffer_read_hex(&out, &hex.blob));
EXPECT_OK(s2n_stuffer_read_hex(&hex, &out));
} else {
EXPECT_ERROR_WITH_ERRNO(
s2n_stuffer_read_hex(&out, &hex.blob),
s2n_stuffer_read_hex(&hex, &out),
S2N_ERR_BAD_HEX);
}
};
@@ -568,14 +555,11 @@ int main(int argc, char **argv)
}
EXPECT_FALSE(s2n_stuffer_data_available(&hex));
} else if (reader_i == S2N_TEST_N) {
DEFER_CLEANUP(struct s2n_stuffer output = { 0 }, s2n_stuffer_free);
EXPECT_SUCCESS(s2n_stuffer_growable_alloc(&output, 0));

hex.blob.size = s2n_stuffer_data_available(&hex);
EXPECT_OK(s2n_stuffer_read_hex(&output, &hex.blob));

EXPECT_EQUAL(s2n_stuffer_data_available(&output), sizeof(values_u8));
EXPECT_BYTEARRAY_EQUAL(values_u8, output.blob.data, sizeof(values_u8));
DEFER_CLEANUP(struct s2n_blob output = { 0 }, s2n_free);
EXPECT_SUCCESS(s2n_alloc(&output, sizeof(values_u8)));
EXPECT_OK(s2n_stuffer_read_hex(&hex, &output));
EXPECT_EQUAL(s2n_stuffer_data_available(&hex), 0);
EXPECT_BYTEARRAY_EQUAL(values_u8, output.data, output.size);
} else {
FAIL_MSG("unknown hex method");
}
13 changes: 7 additions & 6 deletions tls/s2n_fingerprint.c
Original file line number Diff line number Diff line change
@@ -288,12 +288,13 @@ int s2n_client_hello_get_fingerprint_hash(struct s2n_client_hello *ch, s2n_finge
* but s2n_fingerprint_get_hash returns a hex string instead.
* We need to translate back to the raw bytes.
*/
struct s2n_stuffer bytes_out = { 0 };
POSIX_GUARD(s2n_blob_init(&bytes_out.blob, output, max_output_size));
struct s2n_blob hex_in = { 0 };
POSIX_GUARD(s2n_blob_init(&hex_in, hex_hash, hex_hash_size));
POSIX_GUARD_RESULT(s2n_stuffer_read_hex(&bytes_out, &hex_in));
*output_size = s2n_stuffer_data_available(&bytes_out);
struct s2n_blob bytes_out = { 0 };
POSIX_GUARD(s2n_blob_init(&bytes_out, output, MD5_DIGEST_LENGTH));
struct s2n_stuffer hex_in = { 0 };
POSIX_GUARD(s2n_blob_init(&hex_in.blob, hex_hash, hex_hash_size));
POSIX_GUARD(s2n_stuffer_skip_write(&hex_in, hex_hash_size));
POSIX_GUARD_RESULT(s2n_stuffer_read_hex(&hex_in, &bytes_out));
*output_size = bytes_out.size;

POSIX_GUARD(s2n_fingerprint_get_raw_size(&fingerprint, str_size));
return S2N_SUCCESS;
101 changes: 0 additions & 101 deletions utils/s2n_result.c

This file was deleted.

78 changes: 75 additions & 3 deletions utils/s2n_result.h
Original file line number Diff line number Diff line change
@@ -15,6 +15,69 @@

#pragma once

/*
* The goal of s2n_result is to provide a strongly-typed error
* signal value, which provides the compiler with enough information
* to catch bugs.
*
* Historically, s2n has used int to signal errors. This has caused a few issues:
*
* ## GUARD in a function returning integer types
*
* There is no compiler error if `GUARD(nested_call());` is used in a function
* that is meant to return integer type - not a error signal.
*
* ```c
* uint8_t s2n_answer_to_the_ultimate_question() {
* POSIX_GUARD(s2n_sleep_for_years(7500000));
* return 42;
* }
* ```
*
* In this function we intended to return a `uint8_t` but used a
* `GUARD` which will return -1 if the call fails. This can lead to
* very subtle bugs.
*
* ## `GUARD`ing a function returning any integer type
*
* There is no compiler error if `GUARD(nested_call());` is used
* on a function that doesn't actually return an error signal
*
* ```c
* int s2n_deep_thought() {
* POSIX_GUARD(s2n_answer_to_the_ultimate_question());
* return 0;
* }
* ```
*
* In this function we intended guard against a failure of
* `s2n_answer_to_the_ultimate_question` but that function doesn't
* actually return an error signal. Again, this can lead to sublte
* bugs.
*
* ## Ignored error signals
*
* Without the `warn_unused_result` function attribute, the compiler
* provides no warning when forgetting to `GUARD` a function. Missing
* a `GUARD` can lead to subtle bugs.
*
* ```c
* int s2n_answer_to_the_ultimate_question() {
* s2n_sleep_for_years(7500000); // <- THIS SHOULD BE GUARDED!!!
* return 42;
* }
* ```
*
* # Solution
*
* s2n_result provides a newtype declaration, which is popular in
* languages like [Haskell](https://wiki.haskell.org/Newtype) and
* [Rust](https://doc.rust-lang.org/rust-by-example/generics/new_types.html).
*
* Functions that return S2N_RESULT are automatically marked with the
* `warn_unused_result` attribute, which ensures they are GUARDed.
*/

#include <stdbool.h>

#include "api/s2n.h"
@@ -37,10 +100,16 @@ typedef struct {
#endif

/* returns true when the result is S2N_RESULT_OK */
S2N_RESULT_MUST_USE bool s2n_result_is_ok(s2n_result result);
S2N_RESULT_MUST_USE static inline bool s2n_result_is_ok(s2n_result result)
{
return result.__error_signal == S2N_SUCCESS;
}

/* returns true when the result is S2N_RESULT_ERROR */
S2N_RESULT_MUST_USE bool s2n_result_is_error(s2n_result result);
S2N_RESULT_MUST_USE static inline bool s2n_result_is_error(s2n_result result)
{
return result.__error_signal != S2N_SUCCESS;
}

/**
* Ignores the returned result of a function
@@ -50,7 +119,10 @@ S2N_RESULT_MUST_USE bool s2n_result_is_error(s2n_result result);
* should only be used in scenarios where the system state is not affected by
* errors.
*/
void s2n_result_ignore(s2n_result result);
static inline void s2n_result_ignore(s2n_result result)
{
/* noop */
}

/* used in function declarations to signal function fallibility */
#define S2N_RESULT S2N_RESULT_MUST_USE s2n_result

0 comments on commit c0d426c

Please sign in to comment.