Adjust proof tooling to support CBMC v6

With CBMC v6, unwinding assertions are enabled by default, and object
bits no longer need to be set at compile time. Update various build
rules to use the latest template as provided with CBMC starter kit.

Also make sure there are no undefined functions.

.github/workflows/ci.yml

@@ -179,7 +179,7 @@ jobs:
         uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main
         with:
           kissat_tag: latest
-          cbmc_version: "5.95.1"
+          cbmc_version: "6.3.1"
       - run: |
           git submodule update --init --recursive --checkout
           sudo apt-get update

test/cbmc/proofs/HTTPClient_AddHeader/HTTPClient_AddHeader_harness.c

@@ -31,6 +31,19 @@
 
 #include "http_cbmc_state.h"
 
+char * httpHeaderStrncpy( char * pDest,
+                          const char * pSrc,
+                          size_t len,
+                          uint8_t isField );
+
+char * __CPROVER_file_local_core_http_client_c_httpHeaderStrncpy( char * pDest,
+                                                                  const char * pSrc,
+                                                                  size_t len,
+                                                                  uint8_t isField )
+{
+    return httpHeaderStrncpy( pDest, pSrc, len, isField );
+}
+
 void HTTPClient_AddHeader_harness()
 {
     HTTPRequestHeaders_t * pRequestHeaders;

test/cbmc/proofs/HTTPClient_AddHeader/Makefile

@@ -44,7 +44,6 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpParserOnMess
 # This decreases the run-time of the proof. This is safe to do for this proof
 # because HTTPClient_AddHeader does not use the results of the copy later in the
 # function.
-REMOVE_FUNCTION_BODY += strncpy
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpHeaderStrncpy
 
 # strncmp is used to find if there exists "\r\n\r\n" at the end of the header

test/cbmc/proofs/HTTPClient_AddRangeHeader/HTTPClient_AddRangeHeader_harness.c

@@ -31,6 +31,19 @@
 
 #include "http_cbmc_state.h"
 
+char * httpHeaderStrncpy( char * pDest,
+                          const char * pSrc,
+                          size_t len,
+                          uint8_t isField );
+
+char * __CPROVER_file_local_core_http_client_c_httpHeaderStrncpy( char * pDest,
+                                                                  const char * pSrc,
+                                                                  size_t len,
+                                                                  uint8_t isField )
+{
+    return httpHeaderStrncpy( pDest, pSrc, len, isField );
+}
+
 void HTTPClient_AddRangeHeader_harness()
 {
     HTTPRequestHeaders_t * pRequestHeaders;

test/cbmc/proofs/HTTPClient_AddRangeHeader/Makefile

@@ -31,7 +31,6 @@ INCLUDES +=
 # This decreases the run-time of the proof. This is safe to do for this proof
 # because HTTPClient_AddRangeHeader does not use the results of the copy later
 # in the function.
-REMOVE_FUNCTION_BODY += strncpy
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpHeaderStrncpy
 
 # strncmp is used to find if there exists "\r\n\r\n" at the end of the header

test/cbmc/proofs/HTTPClient_ReadHeader/HTTPClient_ReadHeader_harness.c

@@ -31,6 +31,16 @@
 
 #include "http_cbmc_state.h"
 
+void llhttp_init( llhttp_t * parser,
+                  llhttp_type_t type,
+                  const llhttp_settings_t * settings )
+{
+}
+
+void llhttp_settings_init( llhttp_settings_t * settings )
+{
+}
+
 void HTTPClient_ReadHeader_harness()
 {
     HTTPResponse_t * pResponse;

test/cbmc/proofs/HTTPClient_Send/HTTPClient_Send_harness.c

@@ -32,6 +32,40 @@
 #include "transport_interface_stubs.h"
 #include "get_time_stub.h"
 
+void llhttp_init( llhttp_t * parser,
+                  llhttp_type_t type,
+                  const llhttp_settings_t * settings )
+{
+}
+
+void llhttp_settings_init( llhttp_settings_t * settings )
+{
+}
+
+llhttp_errno_t llhttp_get_errno( const llhttp_t * parser )
+{
+    llhttp_errno_t result;
+
+    return result;
+}
+
+void llhttp_resume_after_upgrade( llhttp_t * parser )
+{
+}
+
+char * httpHeaderStrncpy( char * pDest,
+                          const char * pSrc,
+                          size_t len,
+                          uint8_t isField );
+
+char * __CPROVER_file_local_core_http_client_c_httpHeaderStrncpy( char * pDest,
+                                                                  const char * pSrc,
+                                                                  size_t len,
+                                                                  uint8_t isField )
+{
+    return httpHeaderStrncpy( pDest, pSrc, len, isField );
+}
+
 void HTTPClient_Send_harness()
 {
     HTTPRequestHeaders_t * pRequestHeaders;

test/cbmc/proofs/HTTPClient_Send/Makefile

@@ -51,7 +51,6 @@ REMOVE_FUNCTION_BODY += llhttp_settings_init
 # This decreases the run-time of the proof. This is safe to do for this proof
 # because all of the functions, in HTTPClient_Send, that would have used the
 # results of the copy are stubbed out to be proven separately.
-REMOVE_FUNCTION_BODY += strncpy
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_http_client_c_httpHeaderStrncpy
 
 # There is a total of 10 digits in INT32_MAX. These loops are unwound once more