From 464affd3c4858f3289bc4e46ec6cf239ebda3b00 Mon Sep 17 00:00:00 2001
From: Theodore Tsirpanis <teo@tsirpanis.gr>
Date: Tue, 6 Aug 2024 16:28:00 +0300
Subject: [PATCH 01/18] Always set the symbol visibility preset to hidden.

---
 cmake/AwsCFlags.cmake | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

diff --git a/cmake/AwsCFlags.cmake b/cmake/AwsCFlags.cmake
index 470f6db18..13e18bd18 100644
--- a/cmake/AwsCFlags.cmake
+++ b/cmake/AwsCFlags.cmake
@@ -247,13 +247,6 @@ function(aws_set_common_properties target)
         set(_ENABLE_LTO_EXPR OFF)
     endif()
 
-    if(BUILD_SHARED_LIBS)
-        if (NOT MSVC)
-            # this should only be set when building shared libs.
-            list(APPEND AWS_C_FLAGS "-fvisibility=hidden")
-        endif()
-    endif()
-
     if(AWS_ENABLE_TRACING)
         target_link_libraries(${target} PRIVATE ittnotify)
     else()
@@ -264,4 +257,5 @@ function(aws_set_common_properties target)
     target_compile_definitions(${target} PRIVATE ${AWS_C_DEFINES_PRIVATE} PUBLIC ${AWS_C_DEFINES_PUBLIC})
     set_target_properties(${target} PROPERTIES LINKER_LANGUAGE C C_STANDARD 99 C_STANDARD_REQUIRED ON)
     set_target_properties(${target} PROPERTIES INTERPROCEDURAL_OPTIMIZATION ${_ENABLE_LTO_EXPR}>)
+    set_target_properties(${target} PROPERTIES C_VISIBILITY_PRESET hidden CXX_VISIBILITY_PRESET hidden)
 endfunction()

From 82fc2ba647f4e82b130c782c90c9b0d3f5502f4a Mon Sep 17 00:00:00 2001
From: Michael Graeb <graebm@amazon.com>
Date: Wed, 14 Aug 2024 11:55:19 -0700
Subject: [PATCH 02/18] Add function so all projects can set the same common
 CMake policies

---
 CMakeLists.txt        | 10 +---------
 cmake/AwsCFlags.cmake | 18 ++++++++++++++++--
 2 files changed, 17 insertions(+), 11 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index d7cedeef9..20438fec0 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -8,14 +8,6 @@ project(aws-c-common LANGUAGES C VERSION 0.1.0)
 
 message(STATUS "CMake ${CMAKE_VERSION}")
 
-if (POLICY CMP0069)
-    cmake_policy(SET CMP0069 NEW) # Enable LTO/IPO if available in the compiler, see AwsCFlags
-endif()
-
-if (POLICY CMP0077)
-    cmake_policy(SET CMP0077 OLD) # Enable options to get their values from normal variables
-endif()
-
 list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_SOURCE_DIR}/cmake")
 include(AwsCFlags)
 include(AwsCheckHeaders)
@@ -189,7 +181,7 @@ file(GLOB COMMON_SRC
         ${AWS_COMMON_EXTERNAL_SRC}
         )
 
-
+aws_set_common_policies()
 add_library(${PROJECT_NAME} ${COMMON_SRC})
 aws_set_common_properties(${PROJECT_NAME} NO_WEXTRA)
 aws_prepare_symbol_visibility_args(${PROJECT_NAME} "AWS_COMMON")
diff --git a/cmake/AwsCFlags.cmake b/cmake/AwsCFlags.cmake
index 13e18bd18..48dd50343 100644
--- a/cmake/AwsCFlags.cmake
+++ b/cmake/AwsCFlags.cmake
@@ -43,6 +43,20 @@ function(aws_check_posix_lfs extra_flags variable)
     endif()
 endfunction()
 
+# This function sets common CMake policies.
+# Call this before calling add_library() or add_executable().
+function(aws_set_common_policies)
+    # Enable LTO/IPO if available in the compiler
+    if (POLICY CMP0069)
+        cmake_policy(SET CMP0069 NEW)
+    endif()
+
+    # Honor visibility properties for all target types
+    if (POLICY CMP0063)
+        cmake_policy(SET CMP0063 NEW)
+    endif()
+endfunction()
+
 # This function will set all common flags on a target
 # Options:
 #  NO_WGNU: Disable -Wgnu
@@ -231,7 +245,6 @@ function(aws_set_common_properties target)
 
         # try to check whether compiler supports LTO/IPO
         if (POLICY CMP0069)
-            cmake_policy(SET CMP0069 NEW)
             include(CheckIPOSupported OPTIONAL RESULT_VARIABLE ipo_check_exists)
             if (ipo_check_exists)
                 check_ipo_supported(RESULT ipo_supported)
@@ -257,5 +270,6 @@ function(aws_set_common_properties target)
     target_compile_definitions(${target} PRIVATE ${AWS_C_DEFINES_PRIVATE} PUBLIC ${AWS_C_DEFINES_PUBLIC})
     set_target_properties(${target} PROPERTIES LINKER_LANGUAGE C C_STANDARD 99 C_STANDARD_REQUIRED ON)
     set_target_properties(${target} PROPERTIES INTERPROCEDURAL_OPTIMIZATION ${_ENABLE_LTO_EXPR}>)
-    set_target_properties(${target} PROPERTIES C_VISIBILITY_PRESET hidden CXX_VISIBILITY_PRESET hidden)
+    set_target_properties(${target} PROPERTIES C_VISIBILITY_PRESET hidden CXX_VISIBILITY_PRESET hidden
+    set_target_properties(${target} PROPERTIES VISIBILITY_INLINES_HIDDEN ON)
 endfunction()

From bf2dcbd546728e2f50d6df4cf3019d5ddc7e865a Mon Sep 17 00:00:00 2001
From: Michael Graeb <graebm@amazon.com>
Date: Mon, 19 Aug 2024 11:28:17 -0700
Subject: [PATCH 03/18] fix typo

---
 cmake/AwsCFlags.cmake | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/cmake/AwsCFlags.cmake b/cmake/AwsCFlags.cmake
index 48dd50343..644c72792 100644
--- a/cmake/AwsCFlags.cmake
+++ b/cmake/AwsCFlags.cmake
@@ -270,6 +270,5 @@ function(aws_set_common_properties target)
     target_compile_definitions(${target} PRIVATE ${AWS_C_DEFINES_PRIVATE} PUBLIC ${AWS_C_DEFINES_PUBLIC})
     set_target_properties(${target} PROPERTIES LINKER_LANGUAGE C C_STANDARD 99 C_STANDARD_REQUIRED ON)
     set_target_properties(${target} PROPERTIES INTERPROCEDURAL_OPTIMIZATION ${_ENABLE_LTO_EXPR}>)
-    set_target_properties(${target} PROPERTIES C_VISIBILITY_PRESET hidden CXX_VISIBILITY_PRESET hidden
-    set_target_properties(${target} PROPERTIES VISIBILITY_INLINES_HIDDEN ON)
+    set_target_properties(${target} PROPERTIES C_VISIBILITY_PRESET hidden CXX_VISIBILITY_PRESET hidden VISIBILITY_INLINES_HIDDEN ON)
 endfunction()

From 53a446550a722154065193e6e4c67af918124cb5 Mon Sep 17 00:00:00 2001
From: Michael Graeb <graebm@amazon.com>
Date: Mon, 19 Aug 2024 13:17:18 -0700
Subject: [PATCH 04/18] Update required CMake

---
 .../app/src/main/cpp/CMakeLists.txt             |  2 +-
 CMakeLists.txt                                  |  3 +--
 cmake/AwsCFlags.cmake                           | 17 +----------------
 3 files changed, 3 insertions(+), 19 deletions(-)

diff --git a/AWSCRTAndroidTestRunner/app/src/main/cpp/CMakeLists.txt b/AWSCRTAndroidTestRunner/app/src/main/cpp/CMakeLists.txt
index a5e57e30d..63b82ecf9 100644
--- a/AWSCRTAndroidTestRunner/app/src/main/cpp/CMakeLists.txt
+++ b/AWSCRTAndroidTestRunner/app/src/main/cpp/CMakeLists.txt
@@ -3,7 +3,7 @@
 
 # Sets the minimum version of CMake required to build the native library.
 
-cmake_minimum_required(VERSION 3.4.1)
+cmake_minimum_required(VERSION 3.13)
 
 # AWS lib
 set(path_to_common "${CMAKE_CURRENT_LIST_DIR}/../../../../..")
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 20438fec0..0fb1d3084 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,7 +1,7 @@
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: Apache-2.0.
 
-cmake_minimum_required(VERSION 3.0)
+cmake_minimum_required(VERSION 3.13)
 option(ALLOW_CROSS_COMPILED_TESTS "Allow tests to be compiled via cross compile, for use with qemu" OFF)
 
 project(aws-c-common LANGUAGES C VERSION 0.1.0)
@@ -181,7 +181,6 @@ file(GLOB COMMON_SRC
         ${AWS_COMMON_EXTERNAL_SRC}
         )
 
-aws_set_common_policies()
 add_library(${PROJECT_NAME} ${COMMON_SRC})
 aws_set_common_properties(${PROJECT_NAME} NO_WEXTRA)
 aws_prepare_symbol_visibility_args(${PROJECT_NAME} "AWS_COMMON")
diff --git a/cmake/AwsCFlags.cmake b/cmake/AwsCFlags.cmake
index 644c72792..0632514b4 100644
--- a/cmake/AwsCFlags.cmake
+++ b/cmake/AwsCFlags.cmake
@@ -43,20 +43,6 @@ function(aws_check_posix_lfs extra_flags variable)
     endif()
 endfunction()
 
-# This function sets common CMake policies.
-# Call this before calling add_library() or add_executable().
-function(aws_set_common_policies)
-    # Enable LTO/IPO if available in the compiler
-    if (POLICY CMP0069)
-        cmake_policy(SET CMP0069 NEW)
-    endif()
-
-    # Honor visibility properties for all target types
-    if (POLICY CMP0063)
-        cmake_policy(SET CMP0063 NEW)
-    endif()
-endfunction()
-
 # This function will set all common flags on a target
 # Options:
 #  NO_WGNU: Disable -Wgnu
@@ -183,8 +169,7 @@ function(aws_set_common_properties target)
         # If the symbols from libcrypto.a aren't hidden, then SOME function calls use the libcrypto.a implementation
         # and SOME function calls use the libcrypto.so implementation, and this mismatch leads to weird crashes.
         if (UNIX AND NOT APPLE)
-            # If we used target_link_options() (CMake 3.13+) we could make these flags PUBLIC
-            set_property(TARGET ${target} APPEND_STRING PROPERTY LINK_FLAGS " -Wl,--exclude-libs,libcrypto.a")
+            target_link_options(${target} PUBLIC "LINKER:--exclude-libs,libcrypto.a")
         endif()
 
     endif()

From 2608a0464d8f3a2ffd4a69d819bab0e5d2f1c150 Mon Sep 17 00:00:00 2001
From: Michael Graeb <graebm@amazon.com>
Date: Mon, 19 Aug 2024 15:52:41 -0700
Subject: [PATCH 05/18] debug failing memtrace test

---
 tests/memtrace_test.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/memtrace_test.c b/tests/memtrace_test.c
index b3be1b7e9..478b4d7e3 100644
--- a/tests/memtrace_test.c
+++ b/tests/memtrace_test.c
@@ -146,7 +146,7 @@ static int s_test_memtrace_stacks(struct aws_allocator *allocator, void *ctx) {
     /* if this is not a debug build, there may not be symbols, so the test cannot
      * verify if a best effort was made */
 #if defined(DEBUG_BUILD)
-    /* fprintf(stderr, "%s\n", test_logger->log_buffer.buffer); */
+    fprintf(stderr, "---LOGS BEGIN---\n%s\n---LOGS END---\n", test_logger->log_buffer.buffer);
     char s_alloc_1_addr[32];
     char s_alloc_2_addr[32];
     char s_alloc_3_addr[32];

From c4992928261510723b13aafe7340116735473e7f Mon Sep 17 00:00:00 2001
From: Michael Graeb <graebm@amazon.com>
Date: Wed, 21 Aug 2024 18:20:50 +0000
Subject: [PATCH 06/18] Keep symbols visible in Debug builds (and in test
 executables), so that backtraces show more function names

---
 cmake/AwsCFlags.cmake      |  9 +++++++--
 cmake/AwsTestHarness.cmake | 13 +++----------
 tests/memtrace_test.c      | 11 +++++------
 3 files changed, 15 insertions(+), 18 deletions(-)

diff --git a/cmake/AwsCFlags.cmake b/cmake/AwsCFlags.cmake
index 0632514b4..c800aa7ff 100644
--- a/cmake/AwsCFlags.cmake
+++ b/cmake/AwsCFlags.cmake
@@ -4,7 +4,6 @@
 include(CheckCCompilerFlag)
 include(CheckIncludeFile)
 include(CheckSymbolExists)
-include(CMakeParseArguments) # needed for CMake v3.4 and lower
 
 option(AWS_ENABLE_LTO "Enables LTO on libraries. Ensure this is set on all consumed targets, or linking will fail" OFF)
 option(LEGACY_COMPILER_SUPPORT "This enables builds with compiler versions such as gcc 4.1.2. This is not a 'supported' feature; it's just a best effort." OFF)
@@ -255,5 +254,11 @@ function(aws_set_common_properties target)
     target_compile_definitions(${target} PRIVATE ${AWS_C_DEFINES_PRIVATE} PUBLIC ${AWS_C_DEFINES_PUBLIC})
     set_target_properties(${target} PROPERTIES LINKER_LANGUAGE C C_STANDARD 99 C_STANDARD_REQUIRED ON)
     set_target_properties(${target} PROPERTIES INTERPROCEDURAL_OPTIMIZATION ${_ENABLE_LTO_EXPR}>)
-    set_target_properties(${target} PROPERTIES C_VISIBILITY_PRESET hidden CXX_VISIBILITY_PRESET hidden VISIBILITY_INLINES_HIDDEN ON)
+
+    # Don't hide symbols in Debug builds.
+    # We do this so that backtraces are more likely to show function names.
+    # We mostly use backtraces to diagnose memory leaks.
+    if (NOT CMAKE_BUILD_TYPE STREQUAL "Debug")
+        set_target_properties(${target} PROPERTIES C_VISIBILITY_PRESET hidden CXX_VISIBILITY_PRESET hidden VISIBILITY_INLINES_HIDDEN ON)
+    endif ()
 endfunction()
diff --git a/cmake/AwsTestHarness.cmake b/cmake/AwsTestHarness.cmake
index 484b66635..69129a3d8 100644
--- a/cmake/AwsTestHarness.cmake
+++ b/cmake/AwsTestHarness.cmake
@@ -39,16 +39,6 @@ function(generate_test_driver driver_exe_name)
     add_executable(${driver_exe_name} ${CMAKE_CURRENT_BINARY_DIR}/test_runner.c ${TESTS})
     aws_set_common_properties(${driver_exe_name} NO_WEXTRA NO_PEDANTIC)
 
-     # Some versions of CMake (3.9-3.11) generate a test_runner.c file with
-     # a strncpy() call that triggers the "stringop-overflow" warning in GCC 8.1+
-     # This warning doesn't exist until GCC 7 though, so test for it before disabling.
-    if (NOT MSVC)
-        check_c_compiler_flag(-Wno-stringop-overflow HAS_WNO_STRINGOP_OVERFLOW)
-        if (HAS_WNO_STRINGOP_OVERFLOW)
-            SET_SOURCE_FILES_PROPERTIES(test_runner.c PROPERTIES COMPILE_FLAGS -Wno-stringop-overflow)
-        endif()
-    endif()
-
     aws_add_sanitizers(${driver_exe_name} ${${PROJECT_NAME}_SANITIZERS})
 
     target_link_libraries(${driver_exe_name} PRIVATE ${PROJECT_NAME})
@@ -57,6 +47,9 @@ function(generate_test_driver driver_exe_name)
     target_compile_definitions(${driver_exe_name} PRIVATE AWS_UNSTABLE_TESTING_API=1)
     target_include_directories(${driver_exe_name} PRIVATE ${CMAKE_CURRENT_LIST_DIR})
 
+    # Export symbols so that backtraces are more likely to show function names.
+    set_target_properties(${driver_exe_name} PROPERTIES ENABLE_EXPORTS ON)
+
     foreach(name IN LISTS TEST_CASES)
         add_test(${name} ${driver_exe_name} "${name}")
         set_tests_properties("${name}" PROPERTIES SKIP_RETURN_CODE ${SKIP_RETURN_CODE_VALUE})
diff --git a/tests/memtrace_test.c b/tests/memtrace_test.c
index 478b4d7e3..c161752b8 100644
--- a/tests/memtrace_test.c
+++ b/tests/memtrace_test.c
@@ -101,7 +101,7 @@ static int s_test_memtrace_stacks(struct aws_allocator *allocator, void *ctx) {
     /* only bother to run this test if the platform can do a backtrace */
     void *probe_stack[1];
     if (!aws_backtrace(probe_stack, 1)) {
-        return 0;
+        return AWS_OP_SKIP;
     }
 
     test_logger_init(&s_test_logger, allocator, AWS_LL_TRACE, 0);
@@ -146,27 +146,26 @@ static int s_test_memtrace_stacks(struct aws_allocator *allocator, void *ctx) {
     /* if this is not a debug build, there may not be symbols, so the test cannot
      * verify if a best effort was made */
 #if defined(DEBUG_BUILD)
-    fprintf(stderr, "---LOGS BEGIN---\n%s\n---LOGS END---\n", test_logger->log_buffer.buffer);
+    fprintf(stderr, "%s\n", test_logger->log_buffer.buffer);
     char s_alloc_1_addr[32];
     char s_alloc_2_addr[32];
     char s_alloc_3_addr[32];
     char s_alloc_4_addr[32];
 #    if defined(_MSC_VER)
-#        pragma warning(push)
 #        pragma warning(disable : 4054) /* type cast function pointer to data pointer */
+#    endif
+
     snprintf(s_alloc_1_addr, AWS_ARRAY_SIZE(s_alloc_1_addr), "0x%tx", (uintptr_t)(void *)s_alloc_1);
     snprintf(s_alloc_2_addr, AWS_ARRAY_SIZE(s_alloc_2_addr), "0x%tx", (uintptr_t)(void *)s_alloc_2);
     snprintf(s_alloc_3_addr, AWS_ARRAY_SIZE(s_alloc_3_addr), "0x%tx", (uintptr_t)(void *)s_alloc_3);
     snprintf(s_alloc_4_addr, AWS_ARRAY_SIZE(s_alloc_4_addr), "0x%tx", (uintptr_t)(void *)s_alloc_4);
-#        pragma warning(pop)
-#    endif /* defined(_MSC_VER) */
 
     const char *log_buffer = (const char *)test_logger->log_buffer.buffer;
     ASSERT_TRUE(strstr(log_buffer, "s_alloc_1") || strstr(log_buffer, s_alloc_1_addr));
     ASSERT_TRUE(strstr(log_buffer, "s_alloc_2") || strstr(log_buffer, s_alloc_2_addr));
     ASSERT_TRUE(strstr(log_buffer, "s_alloc_3") || strstr(log_buffer, s_alloc_3_addr));
     ASSERT_TRUE(strstr(log_buffer, "s_alloc_4") || strstr(log_buffer, s_alloc_4_addr));
-#endif
+#endif /* DEBUG_BUILD */
 
     /* reset log */
     aws_byte_buf_reset(&test_logger->log_buffer, true);

From ed3b4926895338a2067939631318b7734162808f Mon Sep 17 00:00:00 2001
From: Michael Graeb <graebm@amazon.com>
Date: Fri, 23 Aug 2024 01:19:47 +0000
Subject: [PATCH 07/18] move libcrypto weirdness to aws-c-cal's CMakeLists.txt

---
 cmake/AwsCFlags.cmake | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/cmake/AwsCFlags.cmake b/cmake/AwsCFlags.cmake
index c800aa7ff..8e752d2e4 100644
--- a/cmake/AwsCFlags.cmake
+++ b/cmake/AwsCFlags.cmake
@@ -159,18 +159,6 @@ function(aws_set_common_properties target)
         # This becomes a define in config.h
         set(AWS_HAVE_POSIX_LARGE_FILE_SUPPORT ${HAS_LFS} CACHE BOOL "Posix Large File Support")
 
-        # Hide symbols from libcrypto.a
-        # This avoids problems when an application ends up using both libcrypto.a and libcrypto.so.
-        #
-        # An example of this happening is the aws-c-io tests.
-        # All the C libs are compiled statically, but then a PKCS#11 library is
-        # loaded at runtime which happens to use libcrypto.so from OpenSSL.
-        # If the symbols from libcrypto.a aren't hidden, then SOME function calls use the libcrypto.a implementation
-        # and SOME function calls use the libcrypto.so implementation, and this mismatch leads to weird crashes.
-        if (UNIX AND NOT APPLE)
-            target_link_options(${target} PUBLIC "LINKER:--exclude-libs,libcrypto.a")
-        endif()
-
     endif()
 
     check_include_file(stdint.h HAS_STDINT)

From 484fddaf09b65e97b6577c020a131e9f5bdb1106 Mon Sep 17 00:00:00 2001
From: Michael Graeb <graebm@amazon.com>
Date: Fri, 23 Aug 2024 03:54:01 +0000
Subject: [PATCH 08/18] revert all changes regarding --exclude-libs,libcrypto.a
 I don't have time right now to investigate the impact of this change

---
 cmake/AwsCFlags.cmake | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/cmake/AwsCFlags.cmake b/cmake/AwsCFlags.cmake
index 8e752d2e4..4b73db013 100644
--- a/cmake/AwsCFlags.cmake
+++ b/cmake/AwsCFlags.cmake
@@ -159,6 +159,20 @@ function(aws_set_common_properties target)
         # This becomes a define in config.h
         set(AWS_HAVE_POSIX_LARGE_FILE_SUPPORT ${HAS_LFS} CACHE BOOL "Posix Large File Support")
 
+        # Hide symbols from libcrypto.a
+        # This avoids problems when an application ends up using both libcrypto.a and libcrypto.so.
+        #
+        # An example of this happening is the aws-c-io tests.
+        # All the C libs are compiled statically, but then a PKCS#11 library is
+        # loaded at runtime which happens to use libcrypto.so from OpenSSL.
+        # If the symbols from libcrypto.a aren't hidden, then SOME function calls use the libcrypto.a implementation
+        # and SOME function calls use the libcrypto.so implementation, and this mismatch leads to weird crashes.
+        if (UNIX AND NOT APPLE)
+            # If we used target_link_options() (CMake 3.13+) we could make these flags PUBLIC
+            set_property(TARGET ${target} APPEND_STRING PROPERTY LINK_FLAGS " -Wl,--exclude-libs,libcrypto.a")
+        endif()
+
+
     endif()
 
     check_include_file(stdint.h HAS_STDINT)

From e98c7dd435de407de54b8ae605cfaec7114f8222 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 24 Aug 2024 08:32:19 +0200
Subject: [PATCH 09/18] Makefile.common updates for CBMC (#1148)

---
 verification/cbmc/proofs/Makefile.common | 395 ++++++++++++-----------
 1 file changed, 212 insertions(+), 183 deletions(-)

diff --git a/verification/cbmc/proofs/Makefile.common b/verification/cbmc/proofs/Makefile.common
index e0897c04d..7658ee5b1 100644
--- a/verification/cbmc/proofs/Makefile.common
+++ b/verification/cbmc/proofs/Makefile.common
@@ -4,7 +4,7 @@
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: MIT-0
 
-CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.5
+CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.11
 
 ################################################################
 # The CBMC Starter Kit depends on the files Makefile.common and
@@ -211,10 +211,13 @@ CHECKFLAGS += $(USE_EXTERNAL_SAT_SOLVER)
 
 ifeq ($(strip $(ENABLE_POOLS)),)
   POOL =
+  INIT_POOLS =
 else ifeq ($(strip $(EXPENSIVE)),)
   POOL =
+  INIT_POOLS =
 else
   POOL = --pool expensive
+  INIT_POOLS = --pools expensive:1
 endif
 
 # Similar to the pool feature above. If Litani is new enough, enable
@@ -229,40 +232,45 @@ endif
 #
 # Each variable below controls a specific property checking flag
 # within CBMC. If desired, a property flag can be disabled within
-# a particular proof by nulling the corresponding variable. For
-# instance, the following line:
+# a particular proof by nulling the corresponding variable when CBMC's default
+# is not to perform such checks, or setting to --no-<CHECK>-check when CBMC's
+# default is to perform such checks. For instance, the following lines:
 #
-#     CHECK_FLAG_POINTER_CHECK =
+#     CBMC_FLAG_POINTER_CHECK = --no-pointer-check
+#     CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK =
 #
-# would disable the --pointer-check CBMC flag within:
+# would disable pointer checks and unsigned overflow checks with CBMC flag
+# within:
 #   * an entire project when added to Makefile-project-defines
 #   * a specific proof when added to the harness Makefile
 
-CBMC_FLAG_MALLOC_MAY_FAIL ?= --malloc-may-fail
-CBMC_FLAG_MALLOC_FAIL_NULL ?= --malloc-fail-null
-CBMC_FLAG_BOUNDS_CHECK ?= --bounds-check
+CBMC_FLAG_MALLOC_MAY_FAIL ?= # set to --no-malloc-may-fail to disable
+CBMC_FLAG_BOUNDS_CHECK ?= # set to --no-bounds-check to disable
 CBMC_FLAG_CONVERSION_CHECK ?= --conversion-check
-CBMC_FLAG_DIV_BY_ZERO_CHECK ?= --div-by-zero-check
+CBMC_FLAG_DIV_BY_ZERO_CHECK ?= # set to --no-div-by-zero-check to disable
 CBMC_FLAG_FLOAT_OVERFLOW_CHECK ?= --float-overflow-check
 CBMC_FLAG_NAN_CHECK ?= --nan-check
-CBMC_FLAG_POINTER_CHECK ?= --pointer-check
+CBMC_FLAG_POINTER_CHECK ?= #set to --no-pointer-check to disable
 CBMC_FLAG_POINTER_OVERFLOW_CHECK ?= --pointer-overflow-check
-CBMC_FLAG_POINTER_PRIMITIVE_CHECK ?= --pointer-primitive-check
-CBMC_FLAG_SIGNED_OVERFLOW_CHECK ?= --signed-overflow-check
-CBMC_FLAG_UNDEFINED_SHIFT_CHECK ?= --undefined-shift-check
+CBMC_FLAG_POINTER_PRIMITIVE_CHECK ?= # set to --no-pointer-primitive-check to disable
+CBMC_FLAG_SIGNED_OVERFLOW_CHECK ?= # set to --no-signed-overflow-check to disable
+CBMC_FLAG_UNDEFINED_SHIFT_CHECK ?= # set to --no-undefined-shift-check to disable
 CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK ?= --unsigned-overflow-check
-CBMC_FLAG_UNWINDING_ASSERTIONS ?= --unwinding-assertions
-CBMC_FLAG_UNWIND ?= --unwind 1
+CBMC_FLAG_UNWINDING_ASSERTIONS ?= # set to --no-unwinding-assertions to disable
+CBMC_DEFAULT_UNWIND ?= --unwind 1
 CBMC_FLAG_FLUSH ?= --flush
 
 # CBMC flags used for property checking and coverage checking
 
-CBMCFLAGS += $(CBMC_FLAG_UNWIND) $(CBMC_UNWINDSET) $(CBMC_FLAG_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 --malloc-may-fail --malloc-fail-null
 
 # CBMC flags used for property checking
 
-CHECKFLAGS += $(CBMC_FLAG_MALLOC_MAY_FAIL)
-CHECKFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL)
 CHECKFLAGS += $(CBMC_FLAG_BOUNDS_CHECK)
 CHECKFLAGS += $(CBMC_FLAG_CONVERSION_CHECK)
 CHECKFLAGS += $(CBMC_FLAG_DIV_BY_ZERO_CHECK)
@@ -274,12 +282,6 @@ CHECKFLAGS += $(CBMC_FLAG_POINTER_PRIMITIVE_CHECK)
 CHECKFLAGS += $(CBMC_FLAG_SIGNED_OVERFLOW_CHECK)
 CHECKFLAGS += $(CBMC_FLAG_UNDEFINED_SHIFT_CHECK)
 CHECKFLAGS += $(CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK)
-CHECKFLAGS += $(CBMC_FLAG_UNWINDING_ASSERTIONS)
-
-# CBMC flags used for coverage checking
-
-COVERFLAGS += $(CBMC_FLAG_MALLOC_MAY_FAIL)
-COVERFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL)
 
 # Additional CBMC flag to CBMC control verbosity.
 #
@@ -307,10 +309,13 @@ COVERFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL)
 NONDET_STATIC ?=
 
 # Flags to pass to goto-cc for compilation and linking
-COMPILE_FLAGS ?= -Wall
-LINK_FLAGS ?= -Wall
+COMPILE_FLAGS ?= -Wall -Werror
+LINK_FLAGS ?= -Wall -Werror
 EXPORT_FILE_LOCAL_SYMBOLS ?= --export-file-local-symbols
 
+# During instrumentation, it adds models of C library functions
+ADD_LIBRARY_FLAG := --add-library
+
 # Preprocessor include paths -I...
 INCLUDES ?=
 
@@ -349,9 +354,9 @@ UNWINDSET ?=
 # contracts).  To satisfy this requirement, it may be necessary to
 # unwind some loops before the function contract and loop invariant
 # transformations are applied to the goto program.  This variable
-# EARLY_UNWINDSET is identical to UNWINDSET, and we assume that the
-# loops mentioned in EARLY_UNWINDSET and UNWINDSET are disjoint.
-EARLY_UNWINDSET ?=
+# CPROVER_LIBRARY_UNWINDSET is identical to UNWINDSET, and we assume that the
+# loops mentioned in CPROVER_LIBRARY_UNWINDSET and UNWINDSET are disjoint.
+CPROVER_LIBRARY_UNWINDSET ?=
 
 # CBMC function removal (Normally set set in the proof Makefile)
 #
@@ -396,12 +401,28 @@ PROOF_SOURCES ?=
 # report, making the proof run appear to "hang".
 CBMC_TIMEOUT ?= 21600
 
+# CBMC string abstraction
+#
+# Replace all uses of char * by a struct that carries that string,
+# and also the underlying allocation and the C string length.
+STRING_ABSTRACTION ?=
+ifdef STRING_ABSTRACTION
+  ifneq ($(strip $(STRING_ABSTRACTION)),)
+    CBMC_STRING_ABSTRACTION := --string-abstraction
+  endif
+endif
+
+# Optional configuration library flags
+OPT_CONFIG_LIBRARY ?=
+CBMC_OPT_CONFIG_LIBRARY := $(CBMC_FLAG_MALLOC_MAY_FAIL) $(CBMC_STRING_ABSTRACTION)
+
 # Proof writers could add function contracts in their source code.
 # These contracts are ignored by default, but may be enabled in two distinct
 # contexts using the following two variables:
 # 1. To check whether one or more function contracts are sound with respect to
 #    the function implementation, CHECK_FUNCTION_CONTRACTS should be a list of
-#    function names.
+#    function names. Use CHECK_FUNCTION_CONTRACTS_REC to check contracts on
+#    recursive functions.
 # 2. To replace calls to certain functions with their correspondent function
 #    contracts, USE_FUNCTION_CONTRACTS should be a list of function names.
 #    One must check separately whether a function contract is sound before
@@ -409,17 +430,52 @@ CBMC_TIMEOUT ?= 21600
 CHECK_FUNCTION_CONTRACTS ?=
 CBMC_CHECK_FUNCTION_CONTRACTS := $(patsubst %,--enforce-contract %, $(CHECK_FUNCTION_CONTRACTS))
 
+CHECK_FUNCTION_CONTRACTS_REC ?=
+CBMC_CHECK_FUNCTION_CONTRACTS_REC := $(patsubst %,--enforce-contract-rec %, $(CHECK_FUNCTION_CONTRACTS_REC))
+
 USE_FUNCTION_CONTRACTS ?=
 CBMC_USE_FUNCTION_CONTRACTS := $(patsubst %,--replace-call-with-contract %, $(USE_FUNCTION_CONTRACTS))
 
+CODE_CONTRACTS := $(CHECK_FUNCTION_CONTRACTS)$(USE_FUNCTION_CONTRACTS)$(APPLY_LOOP_CONTRACTS)
+
+# Proof writers may also apply function contracts using the Dynamic Frame
+# Condition Checking (DFCC) mode. For more information on DFCC,
+# please see https://diffblue.github.io/cbmc/contracts-dev-spec-dfcc.html.
+USE_DYNAMIC_FRAMES ?=
+ifdef USE_DYNAMIC_FRAMES
+  ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
+    CBMC_USE_DYNAMIC_FRAMES := $(CBMC_OPT_CONFIG_LIBRARY) --dfcc $(HARNESS_ENTRY) $(CBMC_CHECK_FUNCTION_CONTRACTS_REC)
+  endif
+endif
+
 # Similarly, proof writers could also add loop contracts in their source code
 # to obtain unbounded correctness proofs. Unlike function contracts, loop
 # contracts are not reusable and thus are checked and used simultaneously.
 # These contracts are also ignored by default, but may be enabled by setting
-# the APPLY_LOOP_CONTRACTS variable to 1.
-APPLY_LOOP_CONTRACTS ?= 0
-ifeq ($(APPLY_LOOP_CONTRACTS),1)
-  CBMC_APPLY_LOOP_CONTRACTS ?= --apply-loop-contracts
+# the APPLY_LOOP_CONTRACTS variable.
+APPLY_LOOP_CONTRACTS ?=
+ifdef APPLY_LOOP_CONTRACTS
+  ifneq ($(strip $(APPLY_LOOP_CONTRACTS)),)
+    CBMC_APPLY_LOOP_CONTRACTS := --apply-loop-contracts
+  endif
+endif
+
+# The default unwind should only be used in DFCC mode without loop contracts.
+# When loop contracts are applied, we only unwind specified loops.
+# If any loops remain after loop contracts have been applied, CBMC might try
+# to unwind the program indefinitely, because we do not pass default unwind
+# (i.e., --unwind 1) to CBMC when in DFCC mode.
+# We must not use a default unwind command in DFCC mode, because contract instrumentation
+# introduces loops encoding write set inclusion checks that must be dynamically unwound during
+# symex.
+ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
+ifneq ($(strip $(APPLY_LOOP_CONTRACTS)),)
+  UNWIND_0500_FLAGS=$(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS)
+  UNWIND_0500_DESC="$(PROOF_UID): unwinding specified subset of loops"
+else
+  UNWIND_0500_FLAGS=$(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_FLAG_UNWINDING_ASSERTIONS)
+  UNWIND_0500_DESC="$(PROOF_UID): unwinding all loops"
+endif
 endif
 
 # Silence makefile output (eg, long litani commands) unless VERBOSE is set.
@@ -442,7 +498,6 @@ GOTO_CC ?= goto-cc
 GOTO_INSTRUMENT ?= goto-instrument
 CRANGLER ?= crangler
 VIEWER ?= cbmc-viewer
-MAKE_SOURCE ?= make-source
 VIEWER2 ?= cbmc-viewer
 CMAKE ?= cmake
 
@@ -471,19 +526,28 @@ DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS)
 DEFINES += -DCBMC_MAX_OBJECT_SIZE="(SIZE_MAX>>(CBMC_OBJECT_BITS+1))"
 
 # CI currently assumes cbmc invocation has at most one --unwindset
+
+# UNWINDSET is designed for user code (i.e., proof and project code)
 ifdef UNWINDSET
-  ifneq ($(strip $(UNWINDSET)),"")
+  ifneq ($(strip $(UNWINDSET)),)
     CBMC_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(UNWINDSET)))
   endif
 endif
-ifdef EARLY_UNWINDSET
-  ifneq ($(strip $(EARLY_UNWINDSET)),"")
-    CBMC_EARLY_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(EARLY_UNWINDSET)))
+
+# CPROVER_LIBRARY_UNWINDSET is designed for CPROVER library functions
+ifdef CPROVER_LIBRARY_UNWINDSET
+  ifneq ($(strip $(CPROVER_LIBRARY_UNWINDSET)),)
+    CBMC_CPROVER_LIBRARY_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(CPROVER_LIBRARY_UNWINDSET)))
   endif
 endif
 
 CBMC_REMOVE_FUNCTION_BODY := $(patsubst %,--remove-function-body %, $(REMOVE_FUNCTION_BODY))
-CBMC_RESTRICT_FUNCTION_POINTER := $(patsubst %,--restrict-function-pointer %, $(RESTRICT_FUNCTION_POINTER))
+
+ifdef RESTRICT_FUNCTION_POINTER
+  ifneq ($(strip $(RESTRICT_FUNCTION_POINTER)),)
+    CBMC_RESTRICT_FUNCTION_POINTER := $(patsubst %,--restrict-function-pointer %, $(RESTRICT_FUNCTION_POINTER))
+  endif
+endif
 
 ################################################################
 # Targets for rewriting source files with crangler
@@ -567,7 +631,7 @@ $(REWRITTEN_SOURCES):
 # Build targets that make the relevant .goto files
 
 # Compile project sources
-$(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
+$(PROJECT_GOTO)0100.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
 	$(LITANI) add-job \
 	  --command \
 	    '$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \
@@ -579,7 +643,7 @@ $(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
 	  --description "$(PROOF_UID): building project binary"
 
 # Compile proof sources
-$(PROOF_GOTO)1.goto: $(PROOF_SOURCES)
+$(PROOF_GOTO)0100.goto: $(PROOF_SOURCES)
 	$(LITANI) add-job \
 	  --command \
 	    '$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \
@@ -591,7 +655,7 @@ $(PROOF_GOTO)1.goto: $(PROOF_SOURCES)
 	  --description "$(PROOF_UID): building proof binary"
 
 # Remove function bodies from project sources
-$(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto
+$(PROJECT_GOTO)0200.goto: $(PROJECT_GOTO)0100.goto
 	$(LITANI) add-job \
 	  --command \
 	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \
@@ -603,7 +667,7 @@ $(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto
 	  --description "$(PROOF_UID): removing function bodies from project sources"
 
 # Link project and proof sources into the proof harness
-$(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto
+$(HARNESS_GOTO)0100.goto: $(PROOF_GOTO)0100.goto $(PROJECT_GOTO)0200.goto
 	$(LITANI) add-job \
 	  --command '$(GOTO_CC) $(CBMC_VERBOSITY) --function $(HARNESS_ENTRY) $^ $(LINK_FLAGS) -o $@' \
 	  --inputs $^ \
@@ -614,10 +678,10 @@ $(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto
 	  --description "$(PROOF_UID): linking project to proof"
 
 # Restrict function pointers
-$(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto
+$(HARNESS_GOTO)0200.goto: $(HARNESS_GOTO)0100.goto
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) $^ $@' \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) --remove-function-pointers $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
 	  --stdout-file $(LOGDIR)/restrict_function_pointer-log.txt \
@@ -626,7 +690,17 @@ $(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto
 	  --description "$(PROOF_UID): restricting function pointers in project sources"
 
 # Fill static variable with unconstrained values
-$(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto
+$(HARNESS_GOTO)0300.goto: $(HARNESS_GOTO)0200.goto
+ifneq ($(strip $(CODE_CONTRACTS)),)
+	$(LITANI) add-job \
+	  --command 'cp $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/nondet_static-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): not setting static variables to nondet (will do during contract instrumentation)"
+else
 	$(LITANI) add-job \
 	  --command \
 	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(NONDET_STATIC) $^ $@' \
@@ -636,83 +710,102 @@ $(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto
 	  --pipeline-name "$(PROOF_UID)" \
 	  --ci-stage build \
 	  --description "$(PROOF_UID): setting static variables to nondet"
+endif
 
-# Omit unused functions (sharpens coverage calculations)
-$(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.goto
+# Link CPROVER library if DFCC mode is on
+$(HARNESS_GOTO)0400.goto: $(HARNESS_GOTO)0300.goto
+ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(ADD_LIBRARY_FLAG) $(CBMC_OPT_CONFIG_LIBRARY) $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
-	  --stdout-file $(LOGDIR)/drop_unused_functions-log.txt \
+	  --stdout-file $(LOGDIR)/linking-library-models-log.txt \
 	  --pipeline-name "$(PROOF_UID)" \
 	  --ci-stage build \
-	  --description "$(PROOF_UID): dropping unused functions"
+	  --description "$(PROOF_UID): linking CPROVER library"
+else
+	$(LITANI) add-job \
+	  --command 'cp $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/linking-library-models-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): not linking CPROVER library"
+endif
 
-# Omit initialization of unused global variables (reduces problem size)
-$(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)4.goto
+# Early unwind all loops on DFCC mode; otherwise, only unwind loops in proof and project code
+$(HARNESS_GOTO)0500.goto: $(HARNESS_GOTO)0400.goto
+ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(UNWIND_0500_FLAGS) $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
-	  --stdout-file $(LOGDIR)/slice_global_inits-log.txt \
+	  --stdout-file $(LOGDIR)/unwind_loops-log.txt \
 	  --pipeline-name "$(PROOF_UID)" \
 	  --ci-stage build \
-	  --description "$(PROOF_UID): slicing global initializations"
-
-# Replace function calls with function contracts
-# This must be done before enforcing function contracts,
-# since contract enforcement inlines all function calls.
-$(HARNESS_GOTO)6.goto: $(HARNESS_GOTO)5.goto
+	  --description $(UNWIND_0500_DESC)
+else ifneq ($(strip $(CODE_CONTRACTS)),)
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_USE_FUNCTION_CONTRACTS) $^ $@' \
+		'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
-	  --stdout-file $(LOGDIR)/use_function_contracts-log.txt \
+	  --stdout-file $(LOGDIR)/unwind_loops-log.txt \
 	  --pipeline-name "$(PROOF_UID)" \
 	  --ci-stage build \
-	  --description "$(PROOF_UID): replacing function calls with function contracts"
+	  --description "$(PROOF_UID): unwinding loops in proof and project code"
+else
+	$(LITANI) add-job \
+	  --command 'cp $^ $@' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --stdout-file $(LOGDIR)/unwind_loops-log.txt \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --ci-stage build \
+	  --description "$(PROOF_UID): not unwinding loops"
+endif
 
-# Unwind loops for loop and function contracts
-$(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)6.goto
+# Replace function contracts, check function contracts, instrument for loop contracts
+$(HARNESS_GOTO)0600.goto: $(HARNESS_GOTO)0500.goto
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_EARLY_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \
+	    '$(GOTO_INSTRUMENT) $(CBMC_USE_DYNAMIC_FRAMES) $(NONDET_STATIC) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $(CBMC_USE_FUNCTION_CONTRACTS) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
-	  --stdout-file $(LOGDIR)/unwind_loops-log.txt \
+	  --stdout-file $(LOGDIR)/check_function_contracts-log.txt \
 	  --pipeline-name "$(PROOF_UID)" \
 	  --ci-stage build \
-	  --description "$(PROOF_UID): unwinding loops"
+	  --description "$(PROOF_UID): checking function contracts"
 
-# Apply loop contracts
-$(HARNESS_GOTO)8.goto: $(HARNESS_GOTO)7.goto
+# Omit initialization of unused global variables (reduces problem size)
+$(HARNESS_GOTO)0700.goto: $(HARNESS_GOTO)0600.goto
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
-	  --stdout-file $(LOGDIR)/apply_loop_contracts-log.txt \
+	  --stdout-file $(LOGDIR)/slice_global_inits-log.txt \
 	  --pipeline-name "$(PROOF_UID)" \
 	  --ci-stage build \
-	  --description "$(PROOF_UID): applying loop contracts"
+	  --description "$(PROOF_UID): slicing global initializations"
 
-# Check function contracts
-$(HARNESS_GOTO)9.goto: $(HARNESS_GOTO)8.goto
+# Omit unused functions (sharpens coverage calculations)
+$(HARNESS_GOTO)0800.goto: $(HARNESS_GOTO)0700.goto
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $^ $@' \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
-	  --stdout-file $(LOGDIR)/check_function_contracts-log.txt \
+	  --stdout-file $(LOGDIR)/drop_unused_functions-log.txt \
 	  --pipeline-name "$(PROOF_UID)" \
 	  --ci-stage build \
-	  --description "$(PROOF_UID): checking function contracts"
+	  --description "$(PROOF_UID): dropping unused functions"
 
 # Final name for proof harness
-$(HARNESS_GOTO).goto: $(HARNESS_GOTO)9.goto
+$(HARNESS_GOTO).goto: $(HARNESS_GOTO)0800.goto
 	$(LITANI) add-job \
 	  --command 'cp $< $@' \
 	  --inputs $^ \
@@ -724,11 +817,19 @@ $(HARNESS_GOTO).goto: $(HARNESS_GOTO)9.goto
 ################################################################
 # Targets to run the analysis commands
 
-$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto
+ifdef CBMCFLAGS
+  ifeq ($(strip $(CODE_CONTRACTS)),)
+    CBMCFLAGS += $(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_OPT_CONFIG_LIBRARY)
+  else ifeq ($(strip $(USE_DYNAMIC_FRAMES)),)
+    CBMCFLAGS += $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_OPT_CONFIG_LIBRARY)
+  endif
+endif
+
+$(LOGDIR)/result.xml: $(HARNESS_GOTO).goto
 	$(LITANI) add-job \
 	  $(POOL) \
 	  --command \
-	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace $<' \
+	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace --xml-ui $<' \
 	  --inputs $^ \
 	  --outputs $@ \
 	  --ci-stage test \
@@ -741,11 +842,11 @@ $(LOGDIR)/result.txt: $(HARNESS_GOTO).goto
 	  --stderr-file $(LOGDIR)/result-err-log.txt \
 	  --description "$(PROOF_UID): checking safety properties"
 
-$(LOGDIR)/result.xml: $(HARNESS_GOTO).goto
+$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto
 	$(LITANI) add-job \
 	  $(POOL) \
 	  --command \
-	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace --xml-ui $<' \
+	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace $<' \
 	  --inputs $^ \
 	  --outputs $@ \
 	  --ci-stage test \
@@ -788,54 +889,19 @@ $(LOGDIR)/coverage.xml: $(HARNESS_GOTO).goto
 	  --stderr-file $(LOGDIR)/coverage-err-log.txt \
 	  --description "$(PROOF_UID): calculating coverage"
 
-define VIEWER_CMD
-  $(VIEWER) \
-    --result $(LOGDIR)/result.txt \
-    --block $(LOGDIR)/coverage.xml \
-    --property $(LOGDIR)/property.xml \
-    --srcdir $(SRCDIR) \
-    --goto $(HARNESS_GOTO).goto \
-    --htmldir $(PROOFDIR)/html
-endef
-export VIEWER_CMD
-
-$(PROOFDIR)/html: $(LOGDIR)/result.txt $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml
-	$(LITANI) add-job \
-	  --command "$$VIEWER_CMD" \
-	  --inputs $^ \
-	  --outputs $(PROOFDIR)/html \
-	  --pipeline-name "$(PROOF_UID)" \
-	  --ci-stage report \
-	  --stdout-file $(LOGDIR)/viewer-log.txt \
-	  --description "$(PROOF_UID): generating report"
-
+COVERAGE ?= $(LOGDIR)/coverage.xml
+VIEWER_COVERAGE_FLAG ?= --coverage $(COVERAGE)
 
-# Caution: run make-source before running property and coverage checking
-# The current make-source script removes the goto binary
-$(LOGDIR)/source.json:
-	mkdir -p $(dir $@)
-	$(RM) -r $(GOTODIR)
-	$(MAKE_SOURCE) --srcdir $(SRCDIR) --wkdir $(PROOFDIR) > $@
-	$(RM) -r $(GOTODIR)
-
-define VIEWER2_CMD
-  $(VIEWER2) \
-    --result $(LOGDIR)/result.xml \
-    --coverage $(LOGDIR)/coverage.xml \
-    --property $(LOGDIR)/property.xml \
-    --srcdir $(SRCDIR) \
-    --goto $(HARNESS_GOTO).goto \
-    --reportdir $(PROOFDIR)/report \
-    --config $(PROOFDIR)/cbmc-viewer.json
-endef
-export VIEWER2_CMD
-
-# Omit logs/source.json from report generation until make-sources
-# works correctly with Makefiles that invoke the compiler with
-# mutliple source files at once.
-$(PROOFDIR)/report: $(LOGDIR)/result.xml $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml
+$(PROOFDIR)/report: $(LOGDIR)/result.xml $(LOGDIR)/property.xml $(COVERAGE)
 	$(LITANI) add-job \
-	  --command "$$VIEWER2_CMD" \
+	  --command " $(VIEWER) \
+	    --result $(LOGDIR)/result.xml \
+	    $(VIEWER_COVERAGE_FLAG) \
+	    --property $(LOGDIR)/property.xml \
+	    --srcdir $(SRCDIR) \
+	    --goto $(HARNESS_GOTO).goto \
+	    --reportdir $(PROOFDIR)/report \
+	    --config $(PROOFDIR)/cbmc-viewer.json" \
 	  --inputs $^ \
 	  --outputs $(PROOFDIR)/report \
 	  --pipeline-name "$(PROOF_UID)" \
@@ -858,7 +924,7 @@ litani-path:
 _goto: $(HARNESS_GOTO).goto
 goto:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _goto
 	@ echo Running 'litani build'
@@ -867,7 +933,7 @@ goto:
 _result: $(LOGDIR)/result.txt
 result:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _result
 	@ echo Running 'litani build'
@@ -876,7 +942,7 @@ result:
 _property: $(LOGDIR)/property.xml
 property:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _property
 	@ echo Running 'litani build'
@@ -885,30 +951,26 @@ property:
 _coverage: $(LOGDIR)/coverage.xml
 coverage:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _coverage
 	@ echo Running 'litani build'
 	$(LITANI) run-build
 
-# Choose the invocation of cbmc-viewer depending on which version of
-# cbmc-viewer is installed.  The --version flag is not implemented in
-# version 1 --- it is an "unrecognized argument" --- but it is
-# implemented in version 2.
-_report1: $(PROOFDIR)/html
-_report2: $(PROOFDIR)/report
-_report:
-	(cbmc-viewer --version 2>&1 | grep "unrecognized argument" > /dev/null) && \
-		$(MAKE) -B _report1 || $(MAKE) -B _report2
-
-report report1 report2:
+_report: $(PROOFDIR)/report
+report:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _report
 	@ echo Running 'litani build'
 	$(LITANI) run-build
 
+_report_no_coverage:
+	$(MAKE) COVERAGE="" VIEWER_COVERAGE_FLAG="" _report
+report-no-coverage:
+	$(MAKE) COVERAGE="" VIEWER_COVERAGE_FLAG=" " report
+
 ################################################################
 # Targets to clean up after ourselves
 clean:
@@ -918,7 +980,7 @@ clean:
 	-$(RM) $(REWRITTEN_SOURCES) $(foreach rs,$(REWRITTEN_SOURCES),$(rs).json)
 
 veryclean: clean
-	-$(RM) -r html report
+	-$(RM) -r report
 	-$(RM) -r $(LOGDIR) $(GOTODIR)
 
 .PHONY: \
@@ -926,15 +988,14 @@ veryclean: clean
   _goto \
   _property \
   _report \
-  _report2 \
-  _result \
+  _report_no_coverage \
   clean \
   coverage \
   goto \
   litani-path \
   property \
   report \
-  report2 \
+  report-no-coverage \
   result \
   setup_dependencies \
   testdeps \
@@ -943,38 +1004,6 @@ veryclean: clean
 
 ################################################################
 
-# Rule for generating cbmc-batch.yaml, used by the CI at
-# https://github.com/awslabs/aws-batch-cbmc/
-
-JOB_OS ?= ubuntu16
-JOB_MEMORY ?= 32000
-
-# Proofs that are expected to fail should set EXPECTED to
-# "FAILED" in their Makefile. Values other than SUCCESSFUL
-# or FAILED will cause a CI error.
-EXPECTED ?= SUCCESSFUL
-
-define yaml_encode_options
-	"$(shell echo $(1) | sed 's/ ,/ /g' | sed 's/ /;/g')"
-endef
-
-CI_FLAGS = $(CBMCFLAGS) $(CHECKFLAGS) $(COVERFLAGS)
-
-cbmc-batch.yaml:
-	@$(RM) $@
-	@echo 'build_memory: $(JOB_MEMORY)' > $@
-	@echo 'cbmcflags: $(strip $(call yaml_encode_options,$(CI_FLAGS)))' >> $@
-	@echo 'coverage_memory: $(JOB_MEMORY)' >> $@
-	@echo 'expected: $(EXPECTED)' >> $@
-	@echo 'goto: $(HARNESS_GOTO).goto' >> $@
-	@echo 'jobos: $(JOB_OS)' >> $@
-	@echo 'property_memory: $(JOB_MEMORY)' >> $@
-	@echo 'report_memory: $(JOB_MEMORY)' >> $@
-
-.PHONY: cbmc-batch.yaml
-
-################################################################
-
 # Run "make echo-proof-uid" to print the proof ID of a proof. This can be
 # used by scripts to ensure that every proof has an ID, that there are
 # no duplicates, etc.

From cda9704c80a418f465204628b00b8414b6fc355c Mon Sep 17 00:00:00 2001
From: Michael Graeb <graebm@amazon.com>
Date: Tue, 3 Sep 2024 14:12:08 -0700
Subject: [PATCH 10/18] Run proofs with CBMC 6.2.0 (#1149)

Use latest versions of proof tools
---
 .github/workflows/proof_ci_resources/config.yaml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/proof_ci_resources/config.yaml b/.github/workflows/proof_ci_resources/config.yaml
index 83407e8d9..fb955a76f 100644
--- a/.github/workflows/proof_ci_resources/config.yaml
+++ b/.github/workflows/proof_ci_resources/config.yaml
@@ -1,8 +1,8 @@
 # Use exact versions (instead of "latest") so we're not broken by surprise upgrades.
 cadical-tag: "rel-2.0.0" # tag of latest release: https://github.com/arminbiere/cadical/releases
-cbmc-version: "6.1.0" # semver of latest release: https://github.com/diffblue/cbmc/releases
+cbmc-version: "6.2.0" # semver of latest release: https://github.com/diffblue/cbmc/releases
 cbmc-viewer-version: "3.9" # semver of latest release: https://github.com/model-checking/cbmc-viewer/releases
-kissat-tag: "rel-3.1.1" # tag of latest release: https://github.com/arminbiere/kissat/releases
+kissat-tag: "rel-4.0.0" # tag of latest release: https://github.com/arminbiere/kissat/releases
 litani-version: "1.29.0" # semver of latest release: https://github.com/awslabs/aws-build-accumulator/releases
 proofs-dir: verification/cbmc/proofs
 run-cbmc-proofs-command: ./run-cbmc-proofs.py

From 9582e7fefebeb8d38b07b3614262f5545f02dcd0 Mon Sep 17 00:00:00 2001
From: Dmitriy Musatkin <63878209+DmitriyMusatkin@users.noreply.github.com>
Date: Fri, 6 Sep 2024 12:07:00 -0700
Subject: [PATCH 11/18] Only set mtune neoverse if compiler supports it (#1150)

---
 cmake/AwsSIMD.cmake | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/cmake/AwsSIMD.cmake b/cmake/AwsSIMD.cmake
index 65fce96c7..753e53397 100644
--- a/cmake/AwsSIMD.cmake
+++ b/cmake/AwsSIMD.cmake
@@ -18,7 +18,13 @@ else()
     set(AWS_AVX512vL_FLAG "-mavx512vl")
     set(AWS_CLMUL_FLAG "-mpclmul")
     set(AWS_SSE4_2_FLAG "-msse4.2")
-    set(AWS_ARMv8_1_FLAG "-march=armv8-a+crc+crypto -mtune=neoverse-v1")
+
+    check_c_compiler_flag("-mtune=neoverse-v1" HAVE_MTUNE_NEOVERSE_V1)
+    if (HAVE_MTUNE_NEOVERSE_V1)
+        set(AWS_ARMv8_1_FLAG "-march=armv8-a+crc+crypto -mtune=neoverse-v1")
+    else()
+        set(AWS_ARMv8_1_FLAG "-march=armv8-a+crc+crypto")
+    endif()
     set(WERROR_FLAG "-Werror")
 endif()
 

From dc94351464b126d130cb83dba6f85883815edc23 Mon Sep 17 00:00:00 2001
From: Michael Graeb <graebm@amazon.com>
Date: Mon, 7 Oct 2024 10:04:33 -0700
Subject: [PATCH 12/18] Add comment about tuning for "neoverse-v1" (#1153)

---
 cmake/AwsSIMD.cmake | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/cmake/AwsSIMD.cmake b/cmake/AwsSIMD.cmake
index 753e53397..c9bb3c155 100644
--- a/cmake/AwsSIMD.cmake
+++ b/cmake/AwsSIMD.cmake
@@ -19,6 +19,7 @@ else()
     set(AWS_CLMUL_FLAG "-mpclmul")
     set(AWS_SSE4_2_FLAG "-msse4.2")
 
+    # AWS Graviton3 processors use neoverse-v1
     check_c_compiler_flag("-mtune=neoverse-v1" HAVE_MTUNE_NEOVERSE_V1)
     if (HAVE_MTUNE_NEOVERSE_V1)
         set(AWS_ARMv8_1_FLAG "-march=armv8-a+crc+crypto -mtune=neoverse-v1")
@@ -58,7 +59,7 @@ if (USE_CPU_EXTENSIONS)
             _mm256_permutevar8x32_epi32(vec, vec);
 
             return 0;
-        }"  AWS_HAVE_AVX2_INTRINSICS)          
+        }"  AWS_HAVE_AVX2_INTRINSICS)
 
     check_c_source_compiles("
         #include <immintrin.h>

From e9f38b9b211cbc3c22c901265f7ef27d43306b2b Mon Sep 17 00:00:00 2001
From: Dengke Tang <dengket@amazon.com>
Date: Fri, 11 Oct 2024 15:08:29 -0700
Subject: [PATCH 13/18] [fix] prebuild set CMAKE_PREFIX_PATH properly (#1154)

Co-authored-by: Michael Graeb <graebm@amazon.com>
---
 cmake/AwsPrebuildDependency.cmake | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/cmake/AwsPrebuildDependency.cmake b/cmake/AwsPrebuildDependency.cmake
index c0048f20a..598ea2aa4 100644
--- a/cmake/AwsPrebuildDependency.cmake
+++ b/cmake/AwsPrebuildDependency.cmake
@@ -25,11 +25,13 @@ function(aws_prebuild_dependency)
     set(depInstallDir ${depBinaryDir}/install)
     file(MAKE_DIRECTORY ${depBinaryDir})
 
+    # Convert prefix path from list to escaped string, to be passed on command line
+    string(REPLACE ";" "\\\\;" ESCAPED_PREFIX_PATH "${CMAKE_PREFIX_PATH}")
     # For execute_process to accept a dynamically constructed command, it should be passed in a list format.
-    set(cmakeCommand "COMMAND" "${CMAKE_COMMAND}")
+    set(cmakeCommand "${CMAKE_COMMAND}")
     list(APPEND cmakeCommand -S ${AWS_PREBUILD_SOURCE_DIR})
     list(APPEND cmakeCommand -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE})
-    list(APPEND cmakeCommand -DCMAKE_PREFIX_PATH=${CMAKE_PREFIX_PATH})
+    list(APPEND cmakeCommand -DCMAKE_PREFIX_PATH=${ESCAPED_PREFIX_PATH})
     list(APPEND cmakeCommand -DCMAKE_INSTALL_PREFIX=${depInstallDir})
     list(APPEND cmakeCommand -DCMAKE_INSTALL_RPATH=${CMAKE_INSTALL_RPATH})
     list(APPEND cmakeCommand -DBUILD_SHARED_LIBS=${BUILD_SHARED_LIBS})
@@ -39,11 +41,13 @@ function(aws_prebuild_dependency)
         list(APPEND cmakeCommand ${AWS_PREBUILD_CMAKE_ARGUMENTS})
     endif()
 
-    list(APPEND cmakeCommand WORKING_DIRECTORY ${depBinaryDir})
-    list(APPEND cmakeCommand RESULT_VARIABLE result)
-
     # Configure dependency project.
-    execute_process(${cmakeCommand})
+    execute_process(
+        COMMAND ${cmakeCommand}
+        WORKING_DIRECTORY ${depBinaryDir}
+        RESULT_VARIABLE result
+    )
+
     if (NOT ${result} EQUAL 0)
         message(FATAL_ERROR "Configuration failed for dependency project ${AWS_PREBUILD_DEPENDENCY_NAME}")
     endif()

From 1c55339d5bbf9eced30395d77942954c029017ab Mon Sep 17 00:00:00 2001
From: Waqar Ahmed Khan <waahm7@gmail.com>
Date: Fri, 18 Oct 2024 10:33:59 -0700
Subject: [PATCH 14/18] Update cmake_minimum_required to 3.9

---
 CMakeLists.txt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 0fb1d3084..cbdca2e05 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,7 +1,7 @@
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: Apache-2.0.
 
-cmake_minimum_required(VERSION 3.13)
+cmake_minimum_required(VERSION 3.9)
 option(ALLOW_CROSS_COMPILED_TESTS "Allow tests to be compiled via cross compile, for use with qemu" OFF)
 
 project(aws-c-common LANGUAGES C VERSION 0.1.0)

From cba509a3e828fbfeb09894a78c98c90845ff4700 Mon Sep 17 00:00:00 2001
From: Waqar Ahmed Khan <waahm7@gmail.com>
Date: Fri, 18 Oct 2024 10:57:25 -0700
Subject: [PATCH 15/18] undo changes

---
 .../app/src/main/cpp/CMakeLists.txt                    |  2 +-
 CMakeLists.txt                                         |  4 ++++
 cmake/AwsTestHarness.cmake                             | 10 ++++++++++
 3 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/AWSCRTAndroidTestRunner/app/src/main/cpp/CMakeLists.txt b/AWSCRTAndroidTestRunner/app/src/main/cpp/CMakeLists.txt
index 63b82ecf9..9a91baba4 100644
--- a/AWSCRTAndroidTestRunner/app/src/main/cpp/CMakeLists.txt
+++ b/AWSCRTAndroidTestRunner/app/src/main/cpp/CMakeLists.txt
@@ -3,7 +3,7 @@
 
 # Sets the minimum version of CMake required to build the native library.
 
-cmake_minimum_required(VERSION 3.13)
+cmake_minimum_required(VERSION 3.9)
 
 # AWS lib
 set(path_to_common "${CMAKE_CURRENT_LIST_DIR}/../../../../..")
diff --git a/CMakeLists.txt b/CMakeLists.txt
index cbdca2e05..cb3f28504 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -8,6 +8,10 @@ project(aws-c-common LANGUAGES C VERSION 0.1.0)
 
 message(STATUS "CMake ${CMAKE_VERSION}")
 
+if (POLICY CMP0077)
+    cmake_policy(SET CMP0077 OLD) # Enable options to get their values from normal variables
+endif()
+
 list(APPEND CMAKE_MODULE_PATH "${CMAKE_CURRENT_SOURCE_DIR}/cmake")
 include(AwsCFlags)
 include(AwsCheckHeaders)
diff --git a/cmake/AwsTestHarness.cmake b/cmake/AwsTestHarness.cmake
index 69129a3d8..a63ad61a7 100644
--- a/cmake/AwsTestHarness.cmake
+++ b/cmake/AwsTestHarness.cmake
@@ -39,6 +39,16 @@ function(generate_test_driver driver_exe_name)
     add_executable(${driver_exe_name} ${CMAKE_CURRENT_BINARY_DIR}/test_runner.c ${TESTS})
     aws_set_common_properties(${driver_exe_name} NO_WEXTRA NO_PEDANTIC)
 
+    # Some versions of CMake (3.9-3.11) generate a test_runner.c file with
+    # a strncpy() call that triggers the "stringop-overflow" warning in GCC 8.1+
+    # This warning doesn't exist until GCC 7 though, so test for it before disabling.
+    if (NOT MSVC)
+        check_c_compiler_flag(-Wno-stringop-overflow HAS_WNO_STRINGOP_OVERFLOW)
+        if (HAS_WNO_STRINGOP_OVERFLOW)
+            SET_SOURCE_FILES_PROPERTIES(test_runner.c PROPERTIES COMPILE_FLAGS -Wno-stringop-overflow)
+        endif()
+    endif()
+
     aws_add_sanitizers(${driver_exe_name} ${${PROJECT_NAME}_SANITIZERS})
 
     target_link_libraries(${driver_exe_name} PRIVATE ${PROJECT_NAME})

From 6a5627c5e820503619f7a7b64b7bb66b5f0a1642 Mon Sep 17 00:00:00 2001
From: Waqar Ahmed Khan <waahm7@gmail.com>
Date: Fri, 18 Oct 2024 11:16:05 -0700
Subject: [PATCH 16/18] don't log to err

---
 tests/memtrace_test.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/memtrace_test.c b/tests/memtrace_test.c
index c161752b8..e9a7bd9e0 100644
--- a/tests/memtrace_test.c
+++ b/tests/memtrace_test.c
@@ -146,7 +146,7 @@ static int s_test_memtrace_stacks(struct aws_allocator *allocator, void *ctx) {
     /* if this is not a debug build, there may not be symbols, so the test cannot
      * verify if a best effort was made */
 #if defined(DEBUG_BUILD)
-    fprintf(stderr, "%s\n", test_logger->log_buffer.buffer);
+    /* fprintf(stderr, "%s\n", test_logger->log_buffer.buffer); */
     char s_alloc_1_addr[32];
     char s_alloc_2_addr[32];
     char s_alloc_3_addr[32];

From 3e6fa051b82b187a4205700b3735947989b01351 Mon Sep 17 00:00:00 2001
From: Waqar Ahmed Khan <waahm7@gmail.com>
Date: Fri, 18 Oct 2024 11:19:08 -0700
Subject: [PATCH 17/18] revert

---
 tests/memtrace_test.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/memtrace_test.c b/tests/memtrace_test.c
index e9a7bd9e0..c161752b8 100644
--- a/tests/memtrace_test.c
+++ b/tests/memtrace_test.c
@@ -146,7 +146,7 @@ static int s_test_memtrace_stacks(struct aws_allocator *allocator, void *ctx) {
     /* if this is not a debug build, there may not be symbols, so the test cannot
      * verify if a best effort was made */
 #if defined(DEBUG_BUILD)
-    /* fprintf(stderr, "%s\n", test_logger->log_buffer.buffer); */
+    fprintf(stderr, "%s\n", test_logger->log_buffer.buffer);
     char s_alloc_1_addr[32];
     char s_alloc_2_addr[32];
     char s_alloc_3_addr[32];

From 21880c4fe3387db27bf4a7395fe15c982070e355 Mon Sep 17 00:00:00 2001
From: Waqar Ahmed Khan <waahm7@gmail.com>
Date: Wed, 23 Oct 2024 09:11:24 -0700
Subject: [PATCH 18/18] PR feedback

---
 CMakeLists.txt        |  2 ++
 cmake/AwsCFlags.cmake | 18 +++++++-----------
 2 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index cb3f28504..6d14b0241 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,6 +1,8 @@
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: Apache-2.0.
 
+# As of October 2024, we picked 3.9 as our version because internally we still support RHEL5 and AL2012, and CMake 3.9
+# was the latest version available on those platforms.
 cmake_minimum_required(VERSION 3.9)
 option(ALLOW_CROSS_COMPILED_TESTS "Allow tests to be compiled via cross compile, for use with qemu" OFF)
 
diff --git a/cmake/AwsCFlags.cmake b/cmake/AwsCFlags.cmake
index 4b73db013..18ebb712c 100644
--- a/cmake/AwsCFlags.cmake
+++ b/cmake/AwsCFlags.cmake
@@ -230,17 +230,13 @@ function(aws_set_common_properties target)
         set(_ENABLE_LTO_EXPR $<NOT:$<CONFIG:Debug>>)
 
         # try to check whether compiler supports LTO/IPO
-        if (POLICY CMP0069)
-            include(CheckIPOSupported OPTIONAL RESULT_VARIABLE ipo_check_exists)
-            if (ipo_check_exists)
-                check_ipo_supported(RESULT ipo_supported)
-                if (ipo_supported)
-                    message(STATUS "Enabling IPO/LTO for Release builds")
-                else()
-                    message(STATUS "AWS_ENABLE_LTO is enabled, but cmake/compiler does not support it, disabling")
-                    set(_ENABLE_LTO_EXPR OFF)
-                endif()
-            endif()
+        include(CheckIPOSupported) 
+        check_ipo_supported(RESULT ipo_supported)
+        if (ipo_supported)
+            message(STATUS "Enabling IPO/LTO for Release builds")
+        else()
+            message(STATUS "AWS_ENABLE_LTO is enabled, but cmake/compiler does not support it, disabling")
+            set(_ENABLE_LTO_EXPR OFF)
         endif()
     else()
         set(_ENABLE_LTO_EXPR OFF)