From 9738cc7779e1426ba7379bde01472caec2e29cb2 Mon Sep 17 00:00:00 2001 From: Doug Chapman <54039637+dougch@users.noreply.github.com> Date: Wed, 4 Sep 2024 17:13:35 -0700 Subject: [PATCH 1/4] ci:Al2023 CodeBuild script (#4737) --- codebuild/bin/install_al2_dependencies.sh | 79 +++++++++++++++++------ codebuild/bin/s2n_codebuild_al2.sh | 2 +- 2 files changed, 60 insertions(+), 21 deletions(-) diff --git a/codebuild/bin/install_al2_dependencies.sh b/codebuild/bin/install_al2_dependencies.sh index 55bdf6c3e31..4133bbbc43b 100755 --- a/codebuild/bin/install_al2_dependencies.sh +++ b/codebuild/bin/install_al2_dependencies.sh @@ -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 diff --git a/codebuild/bin/s2n_codebuild_al2.sh b/codebuild/bin/s2n_codebuild_al2.sh index 2f65425eb33..438701028ab 100755 --- a/codebuild/bin/s2n_codebuild_al2.sh +++ b/codebuild/bin/s2n_codebuild_al2.sh @@ -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 From 5328a15e79b15638c3be999d16ad7695d404a275 Mon Sep 17 00:00:00 2001 From: Lindsay Stewart Date: Wed, 4 Sep 2024 19:24:00 -0700 Subject: [PATCH 2/4] refactor: make s2n_stuffer_read_hex match s2n_stuffer_read (#4726) --- stuffer/s2n_stuffer.h | 2 +- stuffer/s2n_stuffer_hex.c | 24 +++---- .../cbmc/proofs/s2n_stuffer_read_hex/Makefile | 2 +- .../s2n_stuffer_read_hex_harness.c | 49 +++++-------- tests/testlib/s2n_hex_testlib.c | 28 ++++---- tests/unit/s2n_self_talk_key_log_test.c | 14 ++-- tests/unit/s2n_stuffer_hex_test.c | 68 +++++++------------ tls/s2n_fingerprint.c | 13 ++-- 8 files changed, 80 insertions(+), 120 deletions(-) diff --git a/stuffer/s2n_stuffer.h b/stuffer/s2n_stuffer.h index c91e5211289..8faff14ef13 100644 --- a/stuffer/s2n_stuffer.h +++ b/stuffer/s2n_stuffer.h @@ -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); diff --git a/stuffer/s2n_stuffer_hex.c b/stuffer/s2n_stuffer_hex.c index c503e31932f..8faf1245abf 100644 --- a/stuffer/s2n_stuffer_hex.c +++ b/stuffer/s2n_stuffer_hex.c @@ -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; } diff --git a/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile index de878adf70e..95f4522e883 100644 --- a/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile @@ -38,6 +38,6 @@ 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 diff --git a/tests/cbmc/proofs/s2n_stuffer_read_hex/s2n_stuffer_read_hex_harness.c b/tests/cbmc/proofs/s2n_stuffer_read_hex/s2n_stuffer_read_hex_harness.c index 4051edc30cf..3abfe5cbc4b 100644 --- a/tests/cbmc/proofs/s2n_stuffer_read_hex/s2n_stuffer_read_hex_harness.c +++ b/tests/cbmc/proofs/s2n_stuffer_read_hex/s2n_stuffer_read_hex_harness.c @@ -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); } diff --git a/tests/testlib/s2n_hex_testlib.c b/tests/testlib/s2n_hex_testlib.c index 0f33b871e25..ba707ea8c67 100644 --- a/tests/testlib/s2n_hex_testlib.c +++ b/tests/testlib/s2n_hex_testlib.c @@ -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; } diff --git a/tests/unit/s2n_self_talk_key_log_test.c b/tests/unit/s2n_self_talk_key_log_test.c index a74d76db310..22e30920ab2 100644 --- a/tests/unit/s2n_self_talk_key_log_test.c +++ b/tests/unit/s2n_self_talk_key_log_test.c @@ -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(); diff --git a/tests/unit/s2n_stuffer_hex_test.c b/tests/unit/s2n_stuffer_hex_test.c index 527e9243c84..9a6cc5cda01 100644 --- a/tests/unit/s2n_stuffer_hex_test.c +++ b/tests/unit/s2n_stuffer_hex_test.c @@ -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"); } diff --git a/tls/s2n_fingerprint.c b/tls/s2n_fingerprint.c index 548a69b34b9..69351e07d77 100644 --- a/tls/s2n_fingerprint.c +++ b/tls/s2n_fingerprint.c @@ -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; From b1d16094ed395816169bc472a3297d009710428f Mon Sep 17 00:00:00 2001 From: Cameron Bytheway Date: Wed, 4 Sep 2024 23:18:26 -0600 Subject: [PATCH 3/4] refactor: move s2n_result functions inline (#4739) --- tests/cbmc/proofs/s2n_alloc/Makefile | 1 - tests/cbmc/proofs/s2n_array_capacity/Makefile | 1 - tests/cbmc/proofs/s2n_array_free/Makefile | 1 - tests/cbmc/proofs/s2n_array_free_p/Makefile | 1 - tests/cbmc/proofs/s2n_array_get/Makefile | 1 - tests/cbmc/proofs/s2n_array_init/Makefile | 1 - tests/cbmc/proofs/s2n_array_insert/Makefile | 1 - .../proofs/s2n_array_insert_and_copy/Makefile | 1 - tests/cbmc/proofs/s2n_array_new/Makefile | 1 - .../proofs/s2n_array_num_elements/Makefile | 1 - tests/cbmc/proofs/s2n_array_pushback/Makefile | 1 - tests/cbmc/proofs/s2n_array_remove/Makefile | 1 - .../proofs/s2n_blob_char_to_lower/Makefile | 1 - tests/cbmc/proofs/s2n_blob_init/Makefile | 1 - .../cbmc/proofs/s2n_blob_is_growable/Makefile | 1 - tests/cbmc/proofs/s2n_blob_slice/Makefile | 1 - tests/cbmc/proofs/s2n_blob_zero/Makefile | 1 - .../Makefile | 1 - .../Makefile | 1 - .../Makefile | 1 - .../s2n_dh_p_g_Ys_to_dh_params/Makefile | 1 - .../proofs/s2n_dh_params_to_p_g_Ys/Makefile | 1 - .../Makefile | 1 - tests/cbmc/proofs/s2n_dup/Makefile | 1 - tests/cbmc/proofs/s2n_free/Makefile | 1 - tests/cbmc/proofs/s2n_free_object/Makefile | 1 - tests/cbmc/proofs/s2n_free_or_wipe/Makefile | 1 - .../s2n_hash_allow_md5_for_fips/Makefile | 1 - .../Makefile | 1 - tests/cbmc/proofs/s2n_hash_copy/Makefile | 1 - tests/cbmc/proofs/s2n_hash_digest/Makefile | 1 - tests/cbmc/proofs/s2n_hash_free/Makefile | 1 - .../Makefile | 1 - tests/cbmc/proofs/s2n_hash_init/Makefile | 1 - .../s2n_hash_is_ready_for_input/Makefile | 1 - tests/cbmc/proofs/s2n_hash_new/Makefile | 1 - tests/cbmc/proofs/s2n_hash_reset/Makefile | 1 - tests/cbmc/proofs/s2n_hash_update/Makefile | 1 - tests/cbmc/proofs/s2n_hmac_copy/Makefile | 1 - tests/cbmc/proofs/s2n_hmac_digest/Makefile | 1 - .../Makefile | 1 - tests/cbmc/proofs/s2n_hmac_free/Makefile | 1 - tests/cbmc/proofs/s2n_hmac_init/Makefile | 1 - tests/cbmc/proofs/s2n_hmac_new/Makefile | 1 - tests/cbmc/proofs/s2n_hmac_reset/Makefile | 1 - .../s2n_hmac_restore_evp_hash_state/Makefile | 1 - .../s2n_hmac_save_evp_hash_state/Makefile | 1 - tests/cbmc/proofs/s2n_hmac_update/Makefile | 1 - .../s2n_is_hello_retry_handshake/Makefile | 1 - .../s2n_is_hello_retry_message/Makefile | 1 - .../proofs/s2n_mul_overflow_harness/Makefile | 1 - .../proofs/s2n_pkcs3_to_dh_params/Makefile | 1 - .../Makefile | 1 - tests/cbmc/proofs/s2n_realloc/Makefile | 1 - tests/cbmc/proofs/s2n_set_add/Makefile | 1 - tests/cbmc/proofs/s2n_set_free/Makefile | 1 - tests/cbmc/proofs/s2n_set_free_p/Makefile | 1 - tests/cbmc/proofs/s2n_set_get/Makefile | 1 - tests/cbmc/proofs/s2n_set_len/Makefile | 1 - tests/cbmc/proofs/s2n_set_new/Makefile | 1 - tests/cbmc/proofs/s2n_set_remove/Makefile | 1 - tests/cbmc/proofs/s2n_socket_write/Makefile | 1 - .../proofs/s2n_socket_write_cork/Makefile | 1 - .../proofs/s2n_socket_write_restore/Makefile | 1 - .../proofs/s2n_socket_write_snapshot/Makefile | 1 - .../proofs/s2n_socket_write_uncork/Makefile | 1 - tests/cbmc/proofs/s2n_stuffer_alloc/Makefile | 1 - .../s2n_stuffer_alloc_ro_from_fd/Makefile | 1 - .../s2n_stuffer_alloc_ro_from_file/Makefile | 1 - .../s2n_stuffer_alloc_ro_from_string/Makefile | 1 - .../s2n_stuffer_certificate_from_pem/Makefile | 1 - tests/cbmc/proofs/s2n_stuffer_copy/Makefile | 1 - .../s2n_stuffer_dhparams_from_pem/Makefile | 1 - .../s2n_stuffer_erase_and_read/Makefile | 1 - .../s2n_stuffer_erase_and_read_bytes/Makefile | 1 - .../proofs/s2n_stuffer_extract_blob/Makefile | 1 - tests/cbmc/proofs/s2n_stuffer_free/Makefile | 1 - .../s2n_stuffer_get_vector_size/Makefile | 1 - .../s2n_stuffer_growable_alloc/Makefile | 1 - tests/cbmc/proofs/s2n_stuffer_init/Makefile | 1 - .../proofs/s2n_stuffer_is_consumed/Makefile | 1 - .../proofs/s2n_stuffer_peek_char/Makefile | 1 - .../s2n_stuffer_peek_check_for_str/Makefile | 1 - tests/cbmc/proofs/s2n_stuffer_printf/Makefile | 1 - .../s2n_stuffer_private_key_from_pem/Makefile | 1 - .../cbmc/proofs/s2n_stuffer_raw_read/Makefile | 1 - .../proofs/s2n_stuffer_raw_write/Makefile | 1 - tests/cbmc/proofs/s2n_stuffer_read/Makefile | 1 - .../proofs/s2n_stuffer_read_base64/Makefile | 1 - .../proofs/s2n_stuffer_read_bytes/Makefile | 1 - .../s2n_stuffer_read_expected_str/Makefile | 1 - .../cbmc/proofs/s2n_stuffer_read_hex/Makefile | 1 - .../proofs/s2n_stuffer_read_line/Makefile | 1 - .../proofs/s2n_stuffer_read_token/Makefile | 1 - .../proofs/s2n_stuffer_read_uint16/Makefile | 1 - .../s2n_stuffer_read_uint16_hex/Makefile | 1 - .../proofs/s2n_stuffer_read_uint24/Makefile | 1 - .../proofs/s2n_stuffer_read_uint32/Makefile | 1 - .../proofs/s2n_stuffer_read_uint64/Makefile | 1 - .../proofs/s2n_stuffer_read_uint8/Makefile | 1 - .../s2n_stuffer_read_uint8_hex/Makefile | 1 - .../proofs/s2n_stuffer_recv_from_fd/Makefile | 1 - tests/cbmc/proofs/s2n_stuffer_reread/Makefile | 1 - .../cbmc/proofs/s2n_stuffer_reserve/Makefile | 1 - .../proofs/s2n_stuffer_reserve_space/Makefile | 1 - .../s2n_stuffer_reserve_uint16/Makefile | 1 - .../s2n_stuffer_reserve_uint24/Makefile | 1 - tests/cbmc/proofs/s2n_stuffer_resize/Makefile | 1 - .../s2n_stuffer_resize_if_empty/Makefile | 1 - .../proofs/s2n_stuffer_rewind_read/Makefile | 1 - .../cbmc/proofs/s2n_stuffer_rewrite/Makefile | 1 - .../proofs/s2n_stuffer_send_to_fd/Makefile | 1 - tests/cbmc/proofs/s2n_stuffer_shift/Makefile | 1 - .../s2n_stuffer_skip_expected_char/Makefile | 1 - .../proofs/s2n_stuffer_skip_read/Makefile | 1 - .../s2n_stuffer_skip_read_until/Makefile | 1 - .../proofs/s2n_stuffer_skip_to_char/Makefile | 1 - .../s2n_stuffer_skip_whitespace/Makefile | 1 - .../proofs/s2n_stuffer_skip_write/Makefile | 1 - tests/cbmc/proofs/s2n_stuffer_wipe/Makefile | 1 - tests/cbmc/proofs/s2n_stuffer_wipe_n/Makefile | 1 - tests/cbmc/proofs/s2n_stuffer_write/Makefile | 1 - .../proofs/s2n_stuffer_write_base64/Makefile | 1 - .../proofs/s2n_stuffer_write_bytes/Makefile | 1 - .../proofs/s2n_stuffer_write_hex/Makefile | 1 - .../s2n_stuffer_write_network_order/Makefile | 1 - .../s2n_stuffer_write_reservation/Makefile | 1 - .../proofs/s2n_stuffer_write_uint16/Makefile | 1 - .../s2n_stuffer_write_uint16_hex/Makefile | 1 - .../proofs/s2n_stuffer_write_uint24/Makefile | 1 - .../proofs/s2n_stuffer_write_uint32/Makefile | 1 - .../proofs/s2n_stuffer_write_uint64/Makefile | 1 - .../proofs/s2n_stuffer_write_uint8/Makefile | 1 - .../s2n_stuffer_write_uint8_hex/Makefile | 1 - .../s2n_stuffer_write_vector_size/Makefile | 1 - .../proofs/s2n_stuffer_writev_bytes/Makefile | 1 - tests/sidetrail/working/s2n-cbc/Makefile | 1 - .../working/s2n-cbc/copy_as_needed.sh | 1 - .../working/s2n-record-read-aead/Makefile | 1 - .../s2n-record-read-aead/copy_as_needed.sh | 1 - .../Makefile | 1 - .../copy_as_needed.sh | 1 - .../working/s2n-record-read-cbc/Makefile | 1 - .../s2n-record-read-cbc/copy_as_needed.sh | 1 - .../s2n-record-read-composite/Makefile | 1 - .../copy_as_needed.sh | 1 - .../working/s2n-record-read-stream/Makefile | 1 - .../s2n-record-read-stream/copy_as_needed.sh | 1 - utils/s2n_result.c | 101 ------------------ utils/s2n_result.h | 78 +++++++++++++- 150 files changed, 75 insertions(+), 252 deletions(-) delete mode 100644 utils/s2n_result.c diff --git a/tests/cbmc/proofs/s2n_alloc/Makefile b/tests/cbmc/proofs/s2n_alloc/Makefile index 7b6c5821968..4f674c25d7a 100644 --- a/tests/cbmc/proofs/s2n_alloc/Makefile +++ b/tests/cbmc/proofs/s2n_alloc/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_array_capacity/Makefile b/tests/cbmc/proofs/s2n_array_capacity/Makefile index 4ba66f28841..642f21c7f77 100644 --- a/tests/cbmc/proofs/s2n_array_capacity/Makefile +++ b/tests/cbmc/proofs/s2n_array_capacity/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_array_free/Makefile b/tests/cbmc/proofs/s2n_array_free/Makefile index e17faa2ef36..9f40b391ddf 100644 --- a/tests/cbmc/proofs/s2n_array_free/Makefile +++ b/tests/cbmc/proofs/s2n_array_free/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_array_free_p/Makefile b/tests/cbmc/proofs/s2n_array_free_p/Makefile index 97e1f3b2476..8dc426f4c92 100644 --- a/tests/cbmc/proofs/s2n_array_free_p/Makefile +++ b/tests/cbmc/proofs/s2n_array_free_p/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_array_get/Makefile b/tests/cbmc/proofs/s2n_array_get/Makefile index a66605b6c2e..cddd3691f80 100644 --- a/tests/cbmc/proofs/s2n_array_get/Makefile +++ b/tests/cbmc/proofs/s2n_array_get/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_array_init/Makefile b/tests/cbmc/proofs/s2n_array_init/Makefile index 48477fd21be..7c409c472de 100644 --- a/tests/cbmc/proofs/s2n_array_init/Makefile +++ b/tests/cbmc/proofs/s2n_array_init/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_array_insert/Makefile b/tests/cbmc/proofs/s2n_array_insert/Makefile index 5a6ed9bc020..76359d7d8b1 100644 --- a/tests/cbmc/proofs/s2n_array_insert/Makefile +++ b/tests/cbmc/proofs/s2n_array_insert/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_array_insert_and_copy/Makefile b/tests/cbmc/proofs/s2n_array_insert_and_copy/Makefile index 3a6c01ca839..b62229ecc10 100644 --- a/tests/cbmc/proofs/s2n_array_insert_and_copy/Makefile +++ b/tests/cbmc/proofs/s2n_array_insert_and_copy/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_array_new/Makefile b/tests/cbmc/proofs/s2n_array_new/Makefile index 87a2c94ac76..a0f1e21699c 100644 --- a/tests/cbmc/proofs/s2n_array_new/Makefile +++ b/tests/cbmc/proofs/s2n_array_new/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_array_num_elements/Makefile b/tests/cbmc/proofs/s2n_array_num_elements/Makefile index d8a1bb65fa6..8eda86bcb64 100644 --- a/tests/cbmc/proofs/s2n_array_num_elements/Makefile +++ b/tests/cbmc/proofs/s2n_array_num_elements/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_array_pushback/Makefile b/tests/cbmc/proofs/s2n_array_pushback/Makefile index 149699b7f0d..2eb48002bbb 100644 --- a/tests/cbmc/proofs/s2n_array_pushback/Makefile +++ b/tests/cbmc/proofs/s2n_array_pushback/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_array_remove/Makefile b/tests/cbmc/proofs/s2n_array_remove/Makefile index 1452adbb608..0d37cb1e52b 100644 --- a/tests/cbmc/proofs/s2n_array_remove/Makefile +++ b/tests/cbmc/proofs/s2n_array_remove/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_blob_char_to_lower/Makefile b/tests/cbmc/proofs/s2n_blob_char_to_lower/Makefile index 7c78a8fd54e..6b360fc687d 100644 --- a/tests/cbmc/proofs/s2n_blob_char_to_lower/Makefile +++ b/tests/cbmc/proofs/s2n_blob_char_to_lower/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_blob_init/Makefile b/tests/cbmc/proofs/s2n_blob_init/Makefile index 6c61d4efcdb..09b60d2a5a8 100644 --- a/tests/cbmc/proofs/s2n_blob_init/Makefile +++ b/tests/cbmc/proofs/s2n_blob_init/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_blob_is_growable/Makefile b/tests/cbmc/proofs/s2n_blob_is_growable/Makefile index c3adc50f277..4923bbee07d 100644 --- a/tests/cbmc/proofs/s2n_blob_is_growable/Makefile +++ b/tests/cbmc/proofs/s2n_blob_is_growable/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_blob_slice/Makefile b/tests/cbmc/proofs/s2n_blob_slice/Makefile index e3e6c95f5fc..c08e425de5c 100644 --- a/tests/cbmc/proofs/s2n_blob_slice/Makefile +++ b/tests/cbmc/proofs/s2n_blob_slice/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_blob_zero/Makefile b/tests/cbmc/proofs/s2n_blob_zero/Makefile index 725f9d36734..d37a04908fb 100644 --- a/tests/cbmc/proofs/s2n_blob_zero/Makefile +++ b/tests/cbmc/proofs/s2n_blob_zero/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_connection_get_last_message_name/Makefile b/tests/cbmc/proofs/s2n_connection_get_last_message_name/Makefile index 92b4a629ada..06ec98fb3ee 100644 --- a/tests/cbmc/proofs/s2n_connection_get_last_message_name/Makefile +++ b/tests/cbmc/proofs/s2n_connection_get_last_message_name/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_client/Makefile b/tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_client/Makefile index 39833089310..5cbafece9e8 100644 --- a/tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_client/Makefile +++ b/tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_client/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_server/Makefile b/tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_server/Makefile index 866f6f441b3..7dc23db2619 100644 --- a/tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_server/Makefile +++ b/tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_server/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_dh_p_g_Ys_to_dh_params/Makefile b/tests/cbmc/proofs/s2n_dh_p_g_Ys_to_dh_params/Makefile index 7c3d58165d5..9d4271143f8 100644 --- a/tests/cbmc/proofs/s2n_dh_p_g_Ys_to_dh_params/Makefile +++ b/tests/cbmc/proofs/s2n_dh_p_g_Ys_to_dh_params/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_dh_params_to_p_g_Ys/Makefile b/tests/cbmc/proofs/s2n_dh_params_to_p_g_Ys/Makefile index 33bba982d1f..53b91ba8f0b 100644 --- a/tests/cbmc/proofs/s2n_dh_params_to_p_g_Ys/Makefile +++ b/tests/cbmc/proofs/s2n_dh_params_to_p_g_Ys/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_digest_is_md5_allowed_for_fips/Makefile b/tests/cbmc/proofs/s2n_digest_is_md5_allowed_for_fips/Makefile index 8eb725fcd8b..18300977db4 100644 --- a/tests/cbmc/proofs/s2n_digest_is_md5_allowed_for_fips/Makefile +++ b/tests/cbmc/proofs/s2n_digest_is_md5_allowed_for_fips/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_dup/Makefile b/tests/cbmc/proofs/s2n_dup/Makefile index 2e98009748e..7c68184aed1 100644 --- a/tests/cbmc/proofs/s2n_dup/Makefile +++ b/tests/cbmc/proofs/s2n_dup/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_free/Makefile b/tests/cbmc/proofs/s2n_free/Makefile index 0d11a263432..d744719eb15 100644 --- a/tests/cbmc/proofs/s2n_free/Makefile +++ b/tests/cbmc/proofs/s2n_free/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_free_object/Makefile b/tests/cbmc/proofs/s2n_free_object/Makefile index 4517211c1d1..45f01074598 100644 --- a/tests/cbmc/proofs/s2n_free_object/Makefile +++ b/tests/cbmc/proofs/s2n_free_object/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_free_or_wipe/Makefile b/tests/cbmc/proofs/s2n_free_or_wipe/Makefile index 3cd080754c1..77dad2f19f0 100644 --- a/tests/cbmc/proofs/s2n_free_or_wipe/Makefile +++ b/tests/cbmc/proofs/s2n_free_or_wipe/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_hash_allow_md5_for_fips/Makefile b/tests/cbmc/proofs/s2n_hash_allow_md5_for_fips/Makefile index e6bdb181f3e..c0c046fd13b 100644 --- a/tests/cbmc/proofs/s2n_hash_allow_md5_for_fips/Makefile +++ b/tests/cbmc/proofs/s2n_hash_allow_md5_for_fips/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_hash_const_time_get_currently_in_hash_block/Makefile b/tests/cbmc/proofs/s2n_hash_const_time_get_currently_in_hash_block/Makefile index d412e4a8db6..3e88a91d608 100644 --- a/tests/cbmc/proofs/s2n_hash_const_time_get_currently_in_hash_block/Makefile +++ b/tests/cbmc/proofs/s2n_hash_const_time_get_currently_in_hash_block/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_hash_copy/Makefile b/tests/cbmc/proofs/s2n_hash_copy/Makefile index 849d7b17200..897a5244557 100644 --- a/tests/cbmc/proofs/s2n_hash_copy/Makefile +++ b/tests/cbmc/proofs/s2n_hash_copy/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_hash_digest/Makefile b/tests/cbmc/proofs/s2n_hash_digest/Makefile index d8a6a67a137..c6a717d3d98 100644 --- a/tests/cbmc/proofs/s2n_hash_digest/Makefile +++ b/tests/cbmc/proofs/s2n_hash_digest/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_hash_free/Makefile b/tests/cbmc/proofs/s2n_hash_free/Makefile index 47028287c60..5156d58ad37 100644 --- a/tests/cbmc/proofs/s2n_hash_free/Makefile +++ b/tests/cbmc/proofs/s2n_hash_free/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_hash_get_currently_in_hash_total/Makefile b/tests/cbmc/proofs/s2n_hash_get_currently_in_hash_total/Makefile index 94bea111004..dd6491d63a4 100644 --- a/tests/cbmc/proofs/s2n_hash_get_currently_in_hash_total/Makefile +++ b/tests/cbmc/proofs/s2n_hash_get_currently_in_hash_total/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_hash_init/Makefile b/tests/cbmc/proofs/s2n_hash_init/Makefile index edc2d08948f..c4e7be3f29e 100644 --- a/tests/cbmc/proofs/s2n_hash_init/Makefile +++ b/tests/cbmc/proofs/s2n_hash_init/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_hash_is_ready_for_input/Makefile b/tests/cbmc/proofs/s2n_hash_is_ready_for_input/Makefile index cf9b6b6179f..7c6abd15dc5 100644 --- a/tests/cbmc/proofs/s2n_hash_is_ready_for_input/Makefile +++ b/tests/cbmc/proofs/s2n_hash_is_ready_for_input/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_hash_new/Makefile b/tests/cbmc/proofs/s2n_hash_new/Makefile index 5367c01a845..3912b92fc81 100644 --- a/tests/cbmc/proofs/s2n_hash_new/Makefile +++ b/tests/cbmc/proofs/s2n_hash_new/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_hash_reset/Makefile b/tests/cbmc/proofs/s2n_hash_reset/Makefile index 74bb0e5767c..495823b32c8 100644 --- a/tests/cbmc/proofs/s2n_hash_reset/Makefile +++ b/tests/cbmc/proofs/s2n_hash_reset/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_hash_update/Makefile b/tests/cbmc/proofs/s2n_hash_update/Makefile index 203d16970a7..df8681c06ba 100644 --- a/tests/cbmc/proofs/s2n_hash_update/Makefile +++ b/tests/cbmc/proofs/s2n_hash_update/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_hmac_copy/Makefile b/tests/cbmc/proofs/s2n_hmac_copy/Makefile index 13ee7e00bf4..9c2e83e70ad 100644 --- a/tests/cbmc/proofs/s2n_hmac_copy/Makefile +++ b/tests/cbmc/proofs/s2n_hmac_copy/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_hmac_digest/Makefile b/tests/cbmc/proofs/s2n_hmac_digest/Makefile index ccec413316e..90781cff1ba 100644 --- a/tests/cbmc/proofs/s2n_hmac_digest/Makefile +++ b/tests/cbmc/proofs/s2n_hmac_digest/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_hmac_digest_two_compression_rounds/Makefile b/tests/cbmc/proofs/s2n_hmac_digest_two_compression_rounds/Makefile index c5b9059bd8a..7fdb8a76da8 100644 --- a/tests/cbmc/proofs/s2n_hmac_digest_two_compression_rounds/Makefile +++ b/tests/cbmc/proofs/s2n_hmac_digest_two_compression_rounds/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_hmac_free/Makefile b/tests/cbmc/proofs/s2n_hmac_free/Makefile index bb614e0ba6c..fd14d427e94 100644 --- a/tests/cbmc/proofs/s2n_hmac_free/Makefile +++ b/tests/cbmc/proofs/s2n_hmac_free/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_hmac_init/Makefile b/tests/cbmc/proofs/s2n_hmac_init/Makefile index 9538174d3a6..c6b1b038ebb 100644 --- a/tests/cbmc/proofs/s2n_hmac_init/Makefile +++ b/tests/cbmc/proofs/s2n_hmac_init/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_hmac_new/Makefile b/tests/cbmc/proofs/s2n_hmac_new/Makefile index 0863e7ecf15..0b293eee7d2 100644 --- a/tests/cbmc/proofs/s2n_hmac_new/Makefile +++ b/tests/cbmc/proofs/s2n_hmac_new/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_hmac_reset/Makefile b/tests/cbmc/proofs/s2n_hmac_reset/Makefile index b7c90ac076e..89373af071c 100644 --- a/tests/cbmc/proofs/s2n_hmac_reset/Makefile +++ b/tests/cbmc/proofs/s2n_hmac_reset/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_hmac_restore_evp_hash_state/Makefile b/tests/cbmc/proofs/s2n_hmac_restore_evp_hash_state/Makefile index a048469a769..bdcb692c930 100644 --- a/tests/cbmc/proofs/s2n_hmac_restore_evp_hash_state/Makefile +++ b/tests/cbmc/proofs/s2n_hmac_restore_evp_hash_state/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_hmac_save_evp_hash_state/Makefile b/tests/cbmc/proofs/s2n_hmac_save_evp_hash_state/Makefile index 6959f5395ed..78ed67bcea6 100644 --- a/tests/cbmc/proofs/s2n_hmac_save_evp_hash_state/Makefile +++ b/tests/cbmc/proofs/s2n_hmac_save_evp_hash_state/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_hmac_update/Makefile b/tests/cbmc/proofs/s2n_hmac_update/Makefile index 70701519f7c..46efbbbb4bd 100644 --- a/tests/cbmc/proofs/s2n_hmac_update/Makefile +++ b/tests/cbmc/proofs/s2n_hmac_update/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_is_hello_retry_handshake/Makefile b/tests/cbmc/proofs/s2n_is_hello_retry_handshake/Makefile index 1af71f502fb..9bb3435f40d 100644 --- a/tests/cbmc/proofs/s2n_is_hello_retry_handshake/Makefile +++ b/tests/cbmc/proofs/s2n_is_hello_retry_handshake/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_is_hello_retry_message/Makefile b/tests/cbmc/proofs/s2n_is_hello_retry_message/Makefile index 31676875859..627888baa9f 100644 --- a/tests/cbmc/proofs/s2n_is_hello_retry_message/Makefile +++ b/tests/cbmc/proofs/s2n_is_hello_retry_message/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_mul_overflow_harness/Makefile b/tests/cbmc/proofs/s2n_mul_overflow_harness/Makefile index 9f2d25e4bcc..ab4f46f28c6 100644 --- a/tests/cbmc/proofs/s2n_mul_overflow_harness/Makefile +++ b/tests/cbmc/proofs/s2n_mul_overflow_harness/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_pkcs3_to_dh_params/Makefile b/tests/cbmc/proofs/s2n_pkcs3_to_dh_params/Makefile index 590b90c02f3..bc6cc1bebf7 100644 --- a/tests/cbmc/proofs/s2n_pkcs3_to_dh_params/Makefile +++ b/tests/cbmc/proofs/s2n_pkcs3_to_dh_params/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_pkcs3_to_dh_params_openssl_1_1_0/Makefile b/tests/cbmc/proofs/s2n_pkcs3_to_dh_params_openssl_1_1_0/Makefile index d07368cc4b1..3bef0e23cc3 100644 --- a/tests/cbmc/proofs/s2n_pkcs3_to_dh_params_openssl_1_1_0/Makefile +++ b/tests/cbmc/proofs/s2n_pkcs3_to_dh_params_openssl_1_1_0/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_realloc/Makefile b/tests/cbmc/proofs/s2n_realloc/Makefile index 9cfce14abb7..ab5e67abe1f 100644 --- a/tests/cbmc/proofs/s2n_realloc/Makefile +++ b/tests/cbmc/proofs/s2n_realloc/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_set_add/Makefile b/tests/cbmc/proofs/s2n_set_add/Makefile index 38aed9682b7..4c331d1ed99 100644 --- a/tests/cbmc/proofs/s2n_set_add/Makefile +++ b/tests/cbmc/proofs/s2n_set_add/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_set_free/Makefile b/tests/cbmc/proofs/s2n_set_free/Makefile index 18706a3ad5f..c98075ef397 100644 --- a/tests/cbmc/proofs/s2n_set_free/Makefile +++ b/tests/cbmc/proofs/s2n_set_free/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_set_free_p/Makefile b/tests/cbmc/proofs/s2n_set_free_p/Makefile index 796b7f92fc3..be9c26b1bd6 100644 --- a/tests/cbmc/proofs/s2n_set_free_p/Makefile +++ b/tests/cbmc/proofs/s2n_set_free_p/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_set_get/Makefile b/tests/cbmc/proofs/s2n_set_get/Makefile index 59cca10e717..a861cbe9746 100644 --- a/tests/cbmc/proofs/s2n_set_get/Makefile +++ b/tests/cbmc/proofs/s2n_set_get/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_set_len/Makefile b/tests/cbmc/proofs/s2n_set_len/Makefile index dc7dca30c88..8527ef4a232 100644 --- a/tests/cbmc/proofs/s2n_set_len/Makefile +++ b/tests/cbmc/proofs/s2n_set_len/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_set_new/Makefile b/tests/cbmc/proofs/s2n_set_new/Makefile index 5cf2f575ea5..55155b43baf 100644 --- a/tests/cbmc/proofs/s2n_set_new/Makefile +++ b/tests/cbmc/proofs/s2n_set_new/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_set_remove/Makefile b/tests/cbmc/proofs/s2n_set_remove/Makefile index 9e5cf9c4700..9e1003af232 100644 --- a/tests/cbmc/proofs/s2n_set_remove/Makefile +++ b/tests/cbmc/proofs/s2n_set_remove/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_socket_write/Makefile b/tests/cbmc/proofs/s2n_socket_write/Makefile index f0ad7340d5b..03b93843e24 100644 --- a/tests/cbmc/proofs/s2n_socket_write/Makefile +++ b/tests/cbmc/proofs/s2n_socket_write/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_socket_write_cork/Makefile b/tests/cbmc/proofs/s2n_socket_write_cork/Makefile index 5d1c3229ea7..ca935eb5438 100644 --- a/tests/cbmc/proofs/s2n_socket_write_cork/Makefile +++ b/tests/cbmc/proofs/s2n_socket_write_cork/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_socket_write_restore/Makefile b/tests/cbmc/proofs/s2n_socket_write_restore/Makefile index 9df51ecf9ec..388537e266e 100644 --- a/tests/cbmc/proofs/s2n_socket_write_restore/Makefile +++ b/tests/cbmc/proofs/s2n_socket_write_restore/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_socket_write_snapshot/Makefile b/tests/cbmc/proofs/s2n_socket_write_snapshot/Makefile index f0acfd8b049..af9c3cdab6b 100644 --- a/tests/cbmc/proofs/s2n_socket_write_snapshot/Makefile +++ b/tests/cbmc/proofs/s2n_socket_write_snapshot/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_socket_write_uncork/Makefile b/tests/cbmc/proofs/s2n_socket_write_uncork/Makefile index 8e6703de20c..a8de536aa05 100644 --- a/tests/cbmc/proofs/s2n_socket_write_uncork/Makefile +++ b/tests/cbmc/proofs/s2n_socket_write_uncork/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_alloc/Makefile b/tests/cbmc/proofs/s2n_stuffer_alloc/Makefile index bba60be57aa..d2bab07c85c 100644 --- a/tests/cbmc/proofs/s2n_stuffer_alloc/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_alloc/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_fd/Makefile b/tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_fd/Makefile index 546413f9bb9..c82e63fa83f 100644 --- a/tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_fd/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_fd/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_file/Makefile b/tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_file/Makefile index 5f765f38972..d6e3ca93c6f 100644 --- a/tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_file/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_file/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_string/Makefile b/tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_string/Makefile index 4973e76a372..86f7cf68fc9 100644 --- a/tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_string/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_string/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_stuffer_certificate_from_pem/Makefile b/tests/cbmc/proofs/s2n_stuffer_certificate_from_pem/Makefile index d66d34d56f0..c19cf955ea8 100644 --- a/tests/cbmc/proofs/s2n_stuffer_certificate_from_pem/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_certificate_from_pem/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_stuffer_copy/Makefile b/tests/cbmc/proofs/s2n_stuffer_copy/Makefile index 78fa8daf14d..8a0ecda1151 100644 --- a/tests/cbmc/proofs/s2n_stuffer_copy/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_copy/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_stuffer_dhparams_from_pem/Makefile b/tests/cbmc/proofs/s2n_stuffer_dhparams_from_pem/Makefile index 0f3db68bee2..5b65d2e8c5e 100644 --- a/tests/cbmc/proofs/s2n_stuffer_dhparams_from_pem/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_dhparams_from_pem/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_stuffer_erase_and_read/Makefile b/tests/cbmc/proofs/s2n_stuffer_erase_and_read/Makefile index 0c70062bbb4..1c584b4559a 100644 --- a/tests/cbmc/proofs/s2n_stuffer_erase_and_read/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_erase_and_read/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_erase_and_read_bytes/Makefile b/tests/cbmc/proofs/s2n_stuffer_erase_and_read_bytes/Makefile index 6dc07ffcb10..00cd843a4a9 100644 --- a/tests/cbmc/proofs/s2n_stuffer_erase_and_read_bytes/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_erase_and_read_bytes/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_extract_blob/Makefile b/tests/cbmc/proofs/s2n_stuffer_extract_blob/Makefile index d756a5b2b32..430d0e3251b 100644 --- a/tests/cbmc/proofs/s2n_stuffer_extract_blob/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_extract_blob/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_stuffer_free/Makefile b/tests/cbmc/proofs/s2n_stuffer_free/Makefile index dbfae88dcf5..44a49f5b297 100644 --- a/tests/cbmc/proofs/s2n_stuffer_free/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_free/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_stuffer_get_vector_size/Makefile b/tests/cbmc/proofs/s2n_stuffer_get_vector_size/Makefile index d53c468edc1..36cda2aa005 100644 --- a/tests/cbmc/proofs/s2n_stuffer_get_vector_size/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_get_vector_size/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_growable_alloc/Makefile b/tests/cbmc/proofs/s2n_stuffer_growable_alloc/Makefile index e1ac1b1dde7..3ed68c7c251 100644 --- a/tests/cbmc/proofs/s2n_stuffer_growable_alloc/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_growable_alloc/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_stuffer_init/Makefile b/tests/cbmc/proofs/s2n_stuffer_init/Makefile index fcb8d398734..8ecd102d33c 100644 --- a/tests/cbmc/proofs/s2n_stuffer_init/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_init/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_is_consumed/Makefile b/tests/cbmc/proofs/s2n_stuffer_is_consumed/Makefile index 2a6f28775df..1e7cb39b652 100644 --- a/tests/cbmc/proofs/s2n_stuffer_is_consumed/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_is_consumed/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_peek_char/Makefile b/tests/cbmc/proofs/s2n_stuffer_peek_char/Makefile index 3fef681dca3..105867e29ba 100644 --- a/tests/cbmc/proofs/s2n_stuffer_peek_char/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_peek_char/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_peek_check_for_str/Makefile b/tests/cbmc/proofs/s2n_stuffer_peek_check_for_str/Makefile index 861199e3a2d..8aebb603758 100644 --- a/tests/cbmc/proofs/s2n_stuffer_peek_check_for_str/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_peek_check_for_str/Makefile @@ -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)) diff --git a/tests/cbmc/proofs/s2n_stuffer_printf/Makefile b/tests/cbmc/proofs/s2n_stuffer_printf/Makefile index 757d05fed98..1b2de1c9556 100644 --- a/tests/cbmc/proofs/s2n_stuffer_printf/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_printf/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_private_key_from_pem/Makefile b/tests/cbmc/proofs/s2n_stuffer_private_key_from_pem/Makefile index 197796980c2..297ee029720 100644 --- a/tests/cbmc/proofs/s2n_stuffer_private_key_from_pem/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_private_key_from_pem/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_raw_read/Makefile b/tests/cbmc/proofs/s2n_stuffer_raw_read/Makefile index 3b9242482ea..18c48f56897 100644 --- a/tests/cbmc/proofs/s2n_stuffer_raw_read/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_raw_read/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_raw_write/Makefile b/tests/cbmc/proofs/s2n_stuffer_raw_write/Makefile index c6eecdec7ef..d33c9e4fc54 100644 --- a/tests/cbmc/proofs/s2n_stuffer_raw_write/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_raw_write/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_stuffer_read/Makefile b/tests/cbmc/proofs/s2n_stuffer_read/Makefile index 1019a31afe6..061b119b482 100644 --- a/tests/cbmc/proofs/s2n_stuffer_read/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_read/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_read_base64/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_base64/Makefile index d58aa0bc120..519c534678f 100644 --- a/tests/cbmc/proofs/s2n_stuffer_read_base64/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_read_base64/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_read_bytes/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_bytes/Makefile index e35d19ade8f..68403e37a03 100644 --- a/tests/cbmc/proofs/s2n_stuffer_read_bytes/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_read_bytes/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_read_expected_str/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_expected_str/Makefile index 12011199941..03480317e53 100644 --- a/tests/cbmc/proofs/s2n_stuffer_read_expected_str/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_read_expected_str/Makefile @@ -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)) diff --git a/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile index 95f4522e883..11ce8f0cec4 100644 --- a/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile @@ -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_read_hex.7:$(MAX_BLOB_SIZE) diff --git a/tests/cbmc/proofs/s2n_stuffer_read_line/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_line/Makefile index af71a41ee48..8bce937df79 100644 --- a/tests/cbmc/proofs/s2n_stuffer_read_line/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_read_line/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_read_token/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_token/Makefile index ab8c054b957..dab4f66eb08 100644 --- a/tests/cbmc/proofs/s2n_stuffer_read_token/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_read_token/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint16/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_uint16/Makefile index e75a84326a2..987a36bb8b1 100644 --- a/tests/cbmc/proofs/s2n_stuffer_read_uint16/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint16/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/Makefile index 1952ae9eb72..f050ae178ef 100644 --- a/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint16_hex/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint24/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_uint24/Makefile index 22ff91e5a39..db02eec2e78 100644 --- a/tests/cbmc/proofs/s2n_stuffer_read_uint24/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint24/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint32/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_uint32/Makefile index c9514376df6..f45af60666f 100644 --- a/tests/cbmc/proofs/s2n_stuffer_read_uint32/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint32/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint64/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_uint64/Makefile index 89a74c565f6..6433d55e305 100644 --- a/tests/cbmc/proofs/s2n_stuffer_read_uint64/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint64/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint8/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_uint8/Makefile index 46920df0de4..a650b8da1c2 100644 --- a/tests/cbmc/proofs/s2n_stuffer_read_uint8/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint8/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/Makefile index 6c05e6c3fdd..701cde4b9bd 100644 --- a/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_read_uint8_hex/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_recv_from_fd/Makefile b/tests/cbmc/proofs/s2n_stuffer_recv_from_fd/Makefile index d1dbe1ec2da..8122a5ebb7e 100644 --- a/tests/cbmc/proofs/s2n_stuffer_recv_from_fd/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_recv_from_fd/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_reread/Makefile b/tests/cbmc/proofs/s2n_stuffer_reread/Makefile index 5a4465149b0..aacbff00427 100644 --- a/tests/cbmc/proofs/s2n_stuffer_reread/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_reread/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_reserve/Makefile b/tests/cbmc/proofs/s2n_stuffer_reserve/Makefile index b60c92f86f6..02826c43ec1 100644 --- a/tests/cbmc/proofs/s2n_stuffer_reserve/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_reserve/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_reserve_space/Makefile b/tests/cbmc/proofs/s2n_stuffer_reserve_space/Makefile index 58669d39a4f..ccda572dfcf 100644 --- a/tests/cbmc/proofs/s2n_stuffer_reserve_space/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_reserve_space/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_reserve_uint16/Makefile b/tests/cbmc/proofs/s2n_stuffer_reserve_uint16/Makefile index 58354660f67..63c4cc091e6 100644 --- a/tests/cbmc/proofs/s2n_stuffer_reserve_uint16/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_reserve_uint16/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_reserve_uint24/Makefile b/tests/cbmc/proofs/s2n_stuffer_reserve_uint24/Makefile index 38f0f17b27a..e65dd8c14ef 100644 --- a/tests/cbmc/proofs/s2n_stuffer_reserve_uint24/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_reserve_uint24/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_resize/Makefile b/tests/cbmc/proofs/s2n_stuffer_resize/Makefile index 4dbaa98db62..3483549b111 100644 --- a/tests/cbmc/proofs/s2n_stuffer_resize/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_resize/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_resize_if_empty/Makefile b/tests/cbmc/proofs/s2n_stuffer_resize_if_empty/Makefile index 5f5e673310d..e5a9f71b8d7 100644 --- a/tests/cbmc/proofs/s2n_stuffer_resize_if_empty/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_resize_if_empty/Makefile @@ -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. diff --git a/tests/cbmc/proofs/s2n_stuffer_rewind_read/Makefile b/tests/cbmc/proofs/s2n_stuffer_rewind_read/Makefile index f34417d6213..6bfb631077f 100644 --- a/tests/cbmc/proofs/s2n_stuffer_rewind_read/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_rewind_read/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_rewrite/Makefile b/tests/cbmc/proofs/s2n_stuffer_rewrite/Makefile index ab87930d122..e3fbbc26648 100644 --- a/tests/cbmc/proofs/s2n_stuffer_rewrite/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_rewrite/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_send_to_fd/Makefile b/tests/cbmc/proofs/s2n_stuffer_send_to_fd/Makefile index 65fd4091856..889a9da2c54 100644 --- a/tests/cbmc/proofs/s2n_stuffer_send_to_fd/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_send_to_fd/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_shift/Makefile b/tests/cbmc/proofs/s2n_stuffer_shift/Makefile index b744029ce30..7c4b70a56f6 100644 --- a/tests/cbmc/proofs/s2n_stuffer_shift/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_shift/Makefile @@ -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)) diff --git a/tests/cbmc/proofs/s2n_stuffer_skip_expected_char/Makefile b/tests/cbmc/proofs/s2n_stuffer_skip_expected_char/Makefile index 4e3b4135029..1212b0e2222 100644 --- a/tests/cbmc/proofs/s2n_stuffer_skip_expected_char/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_skip_expected_char/Makefile @@ -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)) diff --git a/tests/cbmc/proofs/s2n_stuffer_skip_read/Makefile b/tests/cbmc/proofs/s2n_stuffer_skip_read/Makefile index 9a4bb615e1f..57990752c72 100644 --- a/tests/cbmc/proofs/s2n_stuffer_skip_read/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_skip_read/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_skip_read_until/Makefile b/tests/cbmc/proofs/s2n_stuffer_skip_read_until/Makefile index 7a95065ac6e..0d41ae99c7f 100644 --- a/tests/cbmc/proofs/s2n_stuffer_skip_read_until/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_skip_read_until/Makefile @@ -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)) diff --git a/tests/cbmc/proofs/s2n_stuffer_skip_to_char/Makefile b/tests/cbmc/proofs/s2n_stuffer_skip_to_char/Makefile index 64ddf05ce84..1afa3cc55c3 100644 --- a/tests/cbmc/proofs/s2n_stuffer_skip_to_char/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_skip_to_char/Makefile @@ -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)) diff --git a/tests/cbmc/proofs/s2n_stuffer_skip_whitespace/Makefile b/tests/cbmc/proofs/s2n_stuffer_skip_whitespace/Makefile index 9d61761499a..8d7a804ff6d 100644 --- a/tests/cbmc/proofs/s2n_stuffer_skip_whitespace/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_skip_whitespace/Makefile @@ -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)) diff --git a/tests/cbmc/proofs/s2n_stuffer_skip_write/Makefile b/tests/cbmc/proofs/s2n_stuffer_skip_write/Makefile index 933228c81ad..81a669542f4 100644 --- a/tests/cbmc/proofs/s2n_stuffer_skip_write/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_skip_write/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_wipe/Makefile b/tests/cbmc/proofs/s2n_stuffer_wipe/Makefile index ad6d129b71f..ff4874a447b 100644 --- a/tests/cbmc/proofs/s2n_stuffer_wipe/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_wipe/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_wipe_n/Makefile b/tests/cbmc/proofs/s2n_stuffer_wipe_n/Makefile index 13dca870769..582d645aaa9 100644 --- a/tests/cbmc/proofs/s2n_stuffer_wipe_n/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_wipe_n/Makefile @@ -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 += diff --git a/tests/cbmc/proofs/s2n_stuffer_write/Makefile b/tests/cbmc/proofs/s2n_stuffer_write/Makefile index ad39ed44ebb..112a7e34ad3 100644 --- a/tests/cbmc/proofs/s2n_stuffer_write/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_write/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_write_base64/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_base64/Makefile index e8cea785c8b..363bbca7fb1 100644 --- a/tests/cbmc/proofs/s2n_stuffer_write_base64/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_write_base64/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_write_bytes/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_bytes/Makefile index 3bc38d997c8..665df2d85fe 100644 --- a/tests/cbmc/proofs/s2n_stuffer_write_bytes/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_write_bytes/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile index c6c8c1d3974..fce248b599b 100644 --- a/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile @@ -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)) diff --git a/tests/cbmc/proofs/s2n_stuffer_write_network_order/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_network_order/Makefile index 4ac20af933e..8e108734596 100644 --- a/tests/cbmc/proofs/s2n_stuffer_write_network_order/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_write_network_order/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_write_reservation/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_reservation/Makefile index bc921b1d3ee..5e7901ecb07 100644 --- a/tests/cbmc/proofs/s2n_stuffer_write_reservation/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_write_reservation/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint16/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint16/Makefile index 80ad99457f6..ea63e79300b 100644 --- a/tests/cbmc/proofs/s2n_stuffer_write_uint16/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint16/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile index 0fd96bd3162..60a520c84ab 100644 --- a/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint24/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint24/Makefile index d5f36fd153f..1c55bcb2318 100644 --- a/tests/cbmc/proofs/s2n_stuffer_write_uint24/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint24/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint32/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint32/Makefile index c0ef76ced01..710476fffe7 100644 --- a/tests/cbmc/proofs/s2n_stuffer_write_uint32/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint32/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint64/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint64/Makefile index 08465311f7b..9460d5ae5e3 100644 --- a/tests/cbmc/proofs/s2n_stuffer_write_uint64/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint64/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint8/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint8/Makefile index 975c8af6cf9..7406fb430bc 100644 --- a/tests/cbmc/proofs/s2n_stuffer_write_uint8/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint8/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile index b943356821f..5614d875df7 100644 --- a/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_write_vector_size/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_vector_size/Makefile index 350684a0681..744c3d403af 100644 --- a/tests/cbmc/proofs/s2n_stuffer_write_vector_size/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_write_vector_size/Makefile @@ -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 diff --git a/tests/cbmc/proofs/s2n_stuffer_writev_bytes/Makefile b/tests/cbmc/proofs/s2n_stuffer_writev_bytes/Makefile index 6e450fdebc3..43b26efed32 100644 --- a/tests/cbmc/proofs/s2n_stuffer_writev_bytes/Makefile +++ b/tests/cbmc/proofs/s2n_stuffer_writev_bytes/Makefile @@ -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 diff --git a/tests/sidetrail/working/s2n-cbc/Makefile b/tests/sidetrail/working/s2n-cbc/Makefile index 62a55d6807f..bf0b9acc658 100644 --- a/tests/sidetrail/working/s2n-cbc/Makefile +++ b/tests/sidetrail/working/s2n-cbc/Makefile @@ -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 diff --git a/tests/sidetrail/working/s2n-cbc/copy_as_needed.sh b/tests/sidetrail/working/s2n-cbc/copy_as_needed.sh index 641f918c72b..40de4a2f0a1 100755 --- a/tests/sidetrail/working/s2n-cbc/copy_as_needed.sh +++ b/tests/sidetrail/working/s2n-cbc/copy_as_needed.sh @@ -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 diff --git a/tests/sidetrail/working/s2n-record-read-aead/Makefile b/tests/sidetrail/working/s2n-record-read-aead/Makefile index 4bd50938707..f0e4bc5be99 100644 --- a/tests/sidetrail/working/s2n-record-read-aead/Makefile +++ b/tests/sidetrail/working/s2n-record-read-aead/Makefile @@ -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 diff --git a/tests/sidetrail/working/s2n-record-read-aead/copy_as_needed.sh b/tests/sidetrail/working/s2n-record-read-aead/copy_as_needed.sh index ab5aa2777c5..3ad0ef0dead 100755 --- a/tests/sidetrail/working/s2n-record-read-aead/copy_as_needed.sh +++ b/tests/sidetrail/working/s2n-record-read-aead/copy_as_needed.sh @@ -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/ diff --git a/tests/sidetrail/working/s2n-record-read-cbc-negative-test/Makefile b/tests/sidetrail/working/s2n-record-read-cbc-negative-test/Makefile index 789f2756548..33b20a4d7ce 100644 --- a/tests/sidetrail/working/s2n-record-read-cbc-negative-test/Makefile +++ b/tests/sidetrail/working/s2n-record-read-cbc-negative-test/Makefile @@ -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 diff --git a/tests/sidetrail/working/s2n-record-read-cbc-negative-test/copy_as_needed.sh b/tests/sidetrail/working/s2n-record-read-cbc-negative-test/copy_as_needed.sh index 560deb79bb9..be079b67ae4 100755 --- a/tests/sidetrail/working/s2n-record-read-cbc-negative-test/copy_as_needed.sh +++ b/tests/sidetrail/working/s2n-record-read-cbc-negative-test/copy_as_needed.sh @@ -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 diff --git a/tests/sidetrail/working/s2n-record-read-cbc/Makefile b/tests/sidetrail/working/s2n-record-read-cbc/Makefile index 789f2756548..33b20a4d7ce 100644 --- a/tests/sidetrail/working/s2n-record-read-cbc/Makefile +++ b/tests/sidetrail/working/s2n-record-read-cbc/Makefile @@ -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 diff --git a/tests/sidetrail/working/s2n-record-read-cbc/copy_as_needed.sh b/tests/sidetrail/working/s2n-record-read-cbc/copy_as_needed.sh index 560deb79bb9..be079b67ae4 100755 --- a/tests/sidetrail/working/s2n-record-read-cbc/copy_as_needed.sh +++ b/tests/sidetrail/working/s2n-record-read-cbc/copy_as_needed.sh @@ -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 diff --git a/tests/sidetrail/working/s2n-record-read-composite/Makefile b/tests/sidetrail/working/s2n-record-read-composite/Makefile index 6976a64e091..e8735111320 100644 --- a/tests/sidetrail/working/s2n-record-read-composite/Makefile +++ b/tests/sidetrail/working/s2n-record-read-composite/Makefile @@ -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 diff --git a/tests/sidetrail/working/s2n-record-read-composite/copy_as_needed.sh b/tests/sidetrail/working/s2n-record-read-composite/copy_as_needed.sh index de3696c48a8..0ca46755073 100755 --- a/tests/sidetrail/working/s2n-record-read-composite/copy_as_needed.sh +++ b/tests/sidetrail/working/s2n-record-read-composite/copy_as_needed.sh @@ -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 diff --git a/tests/sidetrail/working/s2n-record-read-stream/Makefile b/tests/sidetrail/working/s2n-record-read-stream/Makefile index d44af66e05a..8e0cc2dd20e 100644 --- a/tests/sidetrail/working/s2n-record-read-stream/Makefile +++ b/tests/sidetrail/working/s2n-record-read-stream/Makefile @@ -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 diff --git a/tests/sidetrail/working/s2n-record-read-stream/copy_as_needed.sh b/tests/sidetrail/working/s2n-record-read-stream/copy_as_needed.sh index 7a91cf994f3..9d380cf4b0a 100755 --- a/tests/sidetrail/working/s2n-record-read-stream/copy_as_needed.sh +++ b/tests/sidetrail/working/s2n-record-read-stream/copy_as_needed.sh @@ -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 diff --git a/utils/s2n_result.c b/utils/s2n_result.c deleted file mode 100644 index 47d53f27fbd..00000000000 --- a/utils/s2n_result.c +++ /dev/null @@ -1,101 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * - * Licensed under the Apache License, Version 2.0 (the "License"). - * You may not use this file except in compliance with the License. - * A copy of the License is located at - * - * http://aws.amazon.com/apache2.0 - * - * or in the "license" file accompanying this file. This file is distributed - * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either - * express or implied. See the License for the specific language governing - * permissions and limitations under the License. - */ - -/* - * 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 "utils/s2n_result.h" - -#include - -#include "api/s2n.h" - -/* returns true when the result is S2N_RESULT_OK */ -inline bool s2n_result_is_ok(s2n_result result) -{ - return result.__error_signal == S2N_SUCCESS; -} - -/* returns true when the result is S2N_RESULT_ERROR */ -inline bool s2n_result_is_error(s2n_result result) -{ - return result.__error_signal == S2N_FAILURE; -} - -/* ignores the returned result of a function */ -inline void s2n_result_ignore(s2n_result result) -{ - /* noop */ -} diff --git a/utils/s2n_result.h b/utils/s2n_result.h index 32120a88478..f18ccd3a169 100644 --- a/utils/s2n_result.h +++ b/utils/s2n_result.h @@ -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 #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 From 9964ee729db9c0d592bbe5387933bd9b5c6a26b2 Mon Sep 17 00:00:00 2001 From: Lindsay Stewart Date: Thu, 5 Sep 2024 00:22:37 -0700 Subject: [PATCH 4/4] tests(pcap): fix support for older tshark versions (#4744) --- tests/pcap/Cargo.toml | 2 +- tests/pcap/build.rs | 35 +++++++++++++++++++++++++++ tests/pcap/src/handshake_message.rs | 2 ++ tests/pcap/tests/s2n_client_hellos.rs | 4 +-- 4 files changed, 39 insertions(+), 4 deletions(-) diff --git a/tests/pcap/Cargo.toml b/tests/pcap/Cargo.toml index afb782980ee..917eaaa64da 100644 --- a/tests/pcap/Cargo.toml +++ b/tests/pcap/Cargo.toml @@ -6,7 +6,6 @@ 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] @@ -14,6 +13,7 @@ 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" diff --git a/tests/pcap/build.rs b/tests/pcap/build.rs index 9d809a85962..58fbefeaa61 100644 --- a/tests/pcap/build.rs +++ b/tests/pcap/build.rs @@ -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 { 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"); diff --git a/tests/pcap/src/handshake_message.rs b/tests/pcap/src/handshake_message.rs index 5b2105aeddc..43233acdb6a 100644 --- a/tests/pcap/src/handshake_message.rs +++ b/tests/pcap/src/handshake_message.rs @@ -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 { diff --git a/tests/pcap/tests/s2n_client_hellos.rs b/tests/pcap/tests/s2n_client_hellos.rs index a68293c7092..8e96c575c6b 100644 --- a/tests/pcap/tests/s2n_client_hellos.rs +++ b/tests/pcap/tests/s2n_client_hellos.rs @@ -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> { 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| {