Adjust proof tooling to support CBMC v6

.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