Adopt CBMC 6.1 and cbmc-viewer 3.9

.github/workflows/proof_ci.yaml

@@ -1,6 +1,6 @@
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: MIT-0
-# CBMC starter kit 2.9
+# CBMC starter kit 2.10
 name: Run CBMC proofs
 on:
   push:
@@ -38,11 +38,11 @@ jobs:
       - name: Parse config file
         run: |
           CONFIG_FILE='.github/workflows/proof_ci_resources/config.yaml'
-          for setting in cadical-tag cbmc-version cbmc-viewer-version kissat-tag litani-version proofs-dir run-cbmc-proofs-command; do
+          for setting in cadical-tag cbmc-version cbmc-viewer-version kissat-tag litani-version z3-version bitwuzla-version proofs-dir run-cbmc-proofs-command; do
             VAR=$(echo $setting | tr "[:lower:]" "[:upper:]" | tr - _)
             echo "${VAR}"=$(yq .$setting $CONFIG_FILE) >> $GITHUB_ENV
           done
-      - name: Ensure CBMC, CBMC viewer, Litani versions have been specified
+      - name: Ensure CBMC, CBMC viewer, Litani, Z3, Bitwuzla versions have been specified
         shell: bash
         run: |
           should_exit=false
@@ -58,6 +58,22 @@ jobs:
             echo "You must specify a Litani version (e.g. 'latest' or '1.27.0')"
             should_exit=true
           fi
+          if [ "${{ env.Z3_VERSION }}" == "" ]; then
+            echo "You must specify a Z3 version (e.g. '4.13.0')"
+            should_exit=true
+          fi
+          if [ "${{ env.Z3_VERSION }}" == "latest" ]; then
+            echo "Z3 latest not supported at this time. You must specify an exact Z3 version (e.g. '4.13.0')"
+            should_exit=true
+          fi
+          if [ "${{ env.BITWUZLA_VERSION }}" == "" ]; then
+            echo "You must specify a Bitwuzla version (e.g. '0.5.0')"
+            should_exit=true
+          fi
+          if [ "${{ env.BITWUZLA_VERSION }}" == "latest" ]; then
+            echo "Bitwuzla latest not supported at this time. You must specify an exact version (e.g. '0.5.0')"
+            should_exit=true
+          fi
           if [[ "$should_exit" == true ]]; then exit 1; fi
       - name: Install latest CBMC
         if: ${{ env.CBMC_VERSION == 'latest' }}
@@ -84,15 +100,15 @@ jobs:
         run: |
           CBMC_VIEWER_REL="https://api.github.com/repos/model-checking/cbmc-viewer/releases/latest"
           CBMC_VIEWER_VERSION=$(curl -s $CBMC_VIEWER_REL --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' | jq -r .name | sed  's/viewer-//')
-          pip3 install cbmc-viewer==$CBMC_VIEWER_VERSION
+          sudo pip3 install cbmc-viewer==$CBMC_VIEWER_VERSION
       - name: Install CBMC viewer ${{ env.CBMC_VIEWER_VERSION }}
         if: ${{ env.CBMC_VIEWER_VERSION != 'latest' }}
         shell: bash
         run: |
           sudo apt-get update
           sudo apt-get install --no-install-recommends --yes \
             build-essential universal-ctags
-          pip3 install cbmc-viewer==${{ env.CBMC_VIEWER_VERSION }}
+          sudo pip3 install cbmc-viewer==${{ env.CBMC_VIEWER_VERSION }}
       - name: Install latest Litani
         if: ${{ env.LITANI_VERSION == 'latest' }}
         shell: bash
@@ -114,6 +130,37 @@ jobs:
           sudo apt-get update
           sudo apt-get install --no-install-recommends --yes ./litani.deb
           rm ./litani.deb
+      - name: Install Z3 ${{ env.Z3_VERSION }}
+        if: ${{ env.Z3_VERSION != 'latest' }}
+        shell: bash
+        run: |
+          curl -o z3.zip -L \
+            https://github.com/Z3Prover/z3/releases/download/z3-${{ env.Z3_VERSION }}/z3-${{ env.Z3_VERSION }}-x64-glibc-2.31.zip
+          sudo apt-get install --no-install-recommends --yes unzip
+          unzip z3.zip
+          cd z3-${{ env.Z3_VERSION }}-x64-glibc-2.31/bin \
+            && echo "Adding $(pwd) to PATH for Z3" \
+            && echo "$(pwd)" >> $GITHUB_PATH
+          rm ../../z3.zip
+      - name: Build and Install Bitwuzla ${{ env.BITWUZLA_VERSION }}
+        if: ${{ env.BITWUZLA_VERSION != 'latest' }}
+        shell: bash
+        run: |
+          echo "Installing Bitwuzla dependencies"
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends --yes libgmp-dev cmake
+          sudo pip3 install meson
+          echo "Building Bitwuzla"
+          BITWUZLA_TAG_NAME=${{ env.BITWUZLA_VERSION }}
+          git clone https://github.com/bitwuzla/bitwuzla.git \
+            && cd bitwuzla \
+            && git checkout $BITWUZLA_TAG_NAME \
+            && ./configure.py \
+            && cd build \
+            && ninja;
+          cd src/main \
+            && echo "Adding $(pwd) to PATH for Bitwuzla" \
+            && echo "$(pwd)" >> $GITHUB_PATH
       - name: Install ${{ env.KISSAT_TAG }} kissat
         if: ${{ env.KISSAT_TAG != '' }}
         shell: bash

.github/workflows/proof_ci_resources/config.yaml

@@ -1,7 +1,9 @@
 cadical-tag: latest
-cbmc-version: "5.95.1"
+cbmc-version: "6.1.0"
 cbmc-viewer-version: latest
 kissat-tag: latest
 litani-version: latest
+z3-version: "4.13.0"
+bitwuzla-version: "0.5.0"
 proofs-dir: tests/cbmc/proofs
 run-cbmc-proofs-command: ./run-cbmc-proofs.py

tests/cbmc/proofs/Makefile-project-defines

@@ -46,7 +46,6 @@ CHECKFLAGS += --pointer-primitive-check
 
 # We override abort() to be assert(0)
 PROOF_SOURCES += $(PROOF_STUB)/abort_override_assert_false.c
-REMOVE_FUNCTION_BODY += abort
 
 # Useful for setting unwind limits to one more than some value.
 addone = $(shell echo $$(( $(1) + 1)))

tests/cbmc/proofs/Makefile.common

@@ -259,6 +259,11 @@ CBMC_FLAG_FLUSH ?= --flush
 
 CBMCFLAGS += $(CBMC_FLAG_FLUSH)
 
+# CBMC 6.0.0 enables all standard checks by default, which can make coverage analysis
+# very slow. See https://github.com/diffblue/cbmc/issues/8389
+# For now, we disable these checks when generating coverage info.
+COVERFLAGS ?= --no-standard-checks
+
 # CBMC flags used for property checking
 
 CHECKFLAGS += $(CBMC_FLAG_BOUNDS_CHECK)
@@ -382,6 +387,7 @@ PROJECT_SOURCES ?=
 # PROOF_SOURCES is the list of proof source files to compile, including
 # the proof harness, and including any function stubs being used.
 PROOF_SOURCES ?=
+PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 
 # The number of seconds that CBMC should be allowed to run for before
 # being forcefully terminated. Currently, this is set to be less than
@@ -492,7 +498,6 @@ COMMA :=,
 # Set C compiler defines
 
 CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS)
-COMPILE_FLAGS += --object-bits $(CBMC_OBJECT_BITS)
 
 DEFINES += -DCBMC=1
 DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS)

tests/cbmc/proofs/s2n_array_new/Makefile

@@ -25,6 +25,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/memset_havoc.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c

tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_client/Makefile

@@ -26,6 +26,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c

tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_server/Makefile

@@ -25,9 +25,11 @@ PROOF_SOURCES += $(OPENSSL_SOURCE)/bn_override.c
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
+PROOF_SOURCES += $(PROOF_STUB)/s2n_ensure.c
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_dhe.c
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c

tests/cbmc/proofs/s2n_dh_generate_ephemeral_key/Makefile

@@ -29,6 +29,7 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_dhe.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 UNWINDSET +=
 

tests/cbmc/proofs/s2n_dh_p_g_Ys_to_dh_params/Makefile

@@ -31,6 +31,7 @@ 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 +=
 

tests/cbmc/proofs/s2n_dh_params_check/Makefile

@@ -21,13 +21,15 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(OPENSSL_SOURCE)/dh_override.c
+PROOF_SOURCES += $(OPENSSL_SOURCE)/bn_override.c
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_dhe.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 UNWINDSET +=
 

tests/cbmc/proofs/s2n_dh_params_copy/Makefile

@@ -29,6 +29,7 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_dhe.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 UNWINDSET +=
 

tests/cbmc/proofs/s2n_dh_params_free/Makefile

@@ -29,6 +29,7 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_dhe.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 UNWINDSET +=
 

tests/cbmc/proofs/s2n_free/Makefile

@@ -29,6 +29,7 @@ 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
 

tests/cbmc/proofs/s2n_free_object/Makefile

@@ -28,6 +28,7 @@ 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
 

tests/cbmc/proofs/s2n_free_or_wipe/Makefile

@@ -29,6 +29,7 @@ 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
 

tests/cbmc/proofs/s2n_hash_free/Makefile

@@ -37,7 +37,6 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_init
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_new
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_hash_allow_md5_for_fips
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_allow_md5_for_fips
 
 UNWINDSET +=

tests/cbmc/proofs/s2n_hash_update/Makefile

@@ -36,7 +36,6 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 # We abstract these functions because manual inspection demonstrates they are unreachable.
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_digest
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_hash_digest_size
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_digest
 
 UNWINDSET +=

tests/cbmc/proofs/s2n_hmac_free/Makefile

@@ -23,6 +23,7 @@ PROOF_SOURCES += $(OPENSSL_SOURCE)/bn_override.c
 PROOF_SOURCES += $(OPENSSL_SOURCE)/ec_override.c
 PROOF_SOURCES += $(OPENSSL_SOURCE)/evp_override.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
+PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 
@@ -37,8 +38,6 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_init
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_new
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_hash_allow_md5_for_fips
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_allow_md5_for_fips
 
 UNWINDSET +=
 

tests/cbmc/proofs/s2n_hmac_free/s2n_hmac_free_harness.c

@@ -43,7 +43,7 @@ void s2n_hmac_free_harness()
         assert(state->inner_just_key.hash_impl->free != NULL);
         assert(state->outer.hash_impl->free != NULL);
         assert(state->outer_just_key.hash_impl->free != NULL);
-        
+
         if (s2n_is_in_fips_mode()) {
             assert(state->inner.digest.high_level.evp.ctx == NULL);
             assert(state->inner.digest.high_level.evp_md5_secondary.ctx == NULL);
@@ -93,7 +93,7 @@ void s2n_hmac_free_harness()
          */
         free_rc_keys_from_hash_state(&saved_inner_hash_state);
         free_rc_keys_from_hash_state(&saved_inner_just_key_hash_state);
-        free_rc_keys_from_hash_state(&saved_inner_hash_state);
+        free_rc_keys_from_hash_state(&saved_outer_hash_state);
         free_rc_keys_from_hash_state(&saved_outer_just_key_hash_state);
     }
     /* 3. free our heap-allocated `state` since `s2n_hash_free` only `free`s the contents. */

tests/cbmc/proofs/s2n_hmac_init/Makefile

@@ -17,12 +17,16 @@ PROOF_UID = s2n_hmac_init
 HARNESS_ENTRY = $(PROOF_UID)_harness
 HARNESS_FILE = $(HARNESS_ENTRY).c
 
+CBMC_OBJECT_BITS ?= 10
+
 PROOF_SOURCES += $(OPENSSL_SOURCE)/evp_override.c
 PROOF_SOURCES += $(OPENSSL_SOURCE)/md5_override.c
 PROOF_SOURCES += $(OPENSSL_SOURCE)/sha_override.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
+PROOF_SOURCES += $(PROOF_STUB)/s2n_libcrypto_is_awslc.c
+PROOF_SOURCES += $(PROOF_STUB)/darwin_check_fd_set_overflow.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
@@ -35,15 +39,9 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_new
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_free
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_digest
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_update
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_free
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_new
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_digest
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_update
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_allow_md5_for_fips
-REMOVE_FUNCTION_BODY += s2n_hash_allow_md5_for_fips
 
 # The upper bound limit for these loops is me maximum possible value for xor_pad_size field
 # in struct s2n_hmac_state (128) plus one. See definition for struct s2n_hmac_state

tests/cbmc/proofs/s2n_hmac_update/Makefile

@@ -37,7 +37,6 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 # We abstract these functions because manual inspection demonstrates they are unreachable.
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_digest
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_hash_digest_size
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_digest
 
 UNWINDSET +=

tests/cbmc/proofs/s2n_mem_cleanup/Makefile

@@ -29,8 +29,9 @@ 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_safety.c
 
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
+REMOVE_FUNCTION_BODY +=
 
 UNWINDSET +=
 

tests/cbmc/proofs/s2n_mem_init/Makefile

@@ -22,6 +22,7 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
 
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.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

tests/cbmc/proofs/s2n_stuffer_alloc/Makefile

@@ -26,6 +26,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c

tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_string/Makefile

@@ -24,6 +24,8 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_text.c

tests/cbmc/proofs/s2n_stuffer_copy/Makefile

@@ -24,6 +24,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c