CBMC proof harness type fixes (#510)

tautschnig · web-flow · commit 7a108e80b7cd · 2024-04-17T10:08:58.000-07:00
These changes add necessary forward declarations (or system headers
includes) and address inconsistencies in how we invoke functions from
CBMC proof harnesses as compared to their original signatures.
diff --git a/test/cbmc/proofs/Malloc_FreeRTOS/Malloc_FreeRTOS_harness.c b/test/cbmc/proofs/Malloc_FreeRTOS/Malloc_FreeRTOS_harness.c
@@ -29,6 +29,8 @@
 /*  FreeRTOS includes for OTA library. */
 #include "ota_os_freertos.h"
 
+#include <stdlib.h>
+
 void * pvPortMalloc( size_t size )
 {
     return malloc( size );
diff --git a/test/cbmc/proofs/OTA_CBOR_Decode_GetStreamResponseMessage/OTA_CBOR_Decode_GetStreamResponseMessage_harness.c b/test/cbmc/proofs/OTA_CBOR_Decode_GetStreamResponseMessage/OTA_CBOR_Decode_GetStreamResponseMessage_harness.c
@@ -30,6 +30,8 @@
 #include "cbor.h"
 #include "ota_cbor_private.h"
 
+#include <stdlib.h>
+
 /* Stub to return CBORerror type. */
 CborError returnCborError()
 {
diff --git a/test/cbmc/proofs/OTA_GetStatistics/OTA_GetStatistics_harness.c b/test/cbmc/proofs/OTA_GetStatistics/OTA_GetStatistics_harness.c
@@ -29,6 +29,8 @@
 /*  Ota Agent includes. */
 #include "ota.h"
 
+#include <stdlib.h>
+
 void OTA_GetStatistics_harness()
 {
     OtaErr_t err;
diff --git a/test/cbmc/proofs/OtaReceiveEvent_FreeRTOS/OtaReceiveEvent_FreeRTOS_harness.c b/test/cbmc/proofs/OtaReceiveEvent_FreeRTOS/OtaReceiveEvent_FreeRTOS_harness.c
@@ -31,11 +31,12 @@
 #include "ota_private.h"
 #include "FreeRTOSConfig.h"
 
+#include <stdlib.h>
+
 void OtaReceiveEvent_FreeRTOS_harness()
 {
     OtaEventContext_t * pEventCtx;
     OtaOsStatus_t osStatus;
-    void * pEventMsg;
     uint32_t timeout;
 
     void * pEventMsg = ( void * ) malloc( sizeof( OtaEventMsg_t ) );
diff --git a/test/cbmc/proofs/OtaStartTimer_FreeRTOS/OtaStartTimer_FreeRTOS_harness.c b/test/cbmc/proofs/OtaStartTimer_FreeRTOS/OtaStartTimer_FreeRTOS_harness.c
@@ -30,6 +30,8 @@
 #include "ota_os_freertos.h"
 #include "FreeRTOSConfig.h"
 
+#include <stdlib.h>
+
 void otaCallback( OtaTimerId_t otaTimerId )
 {
     __CPROVER_assert( otaTimerId == OtaRequestTimer || otaTimerId == OtaSelfTestTimer,
diff --git a/test/cbmc/proofs/Posix_OtaReceiveEvent/Posix_OtaReceiveEvent_harness.c b/test/cbmc/proofs/Posix_OtaReceiveEvent/Posix_OtaReceiveEvent_harness.c
@@ -35,6 +35,8 @@
 #include <poll.h>
 #include <mqueue.h>
 
+int nondet_int();
+
 /* Counter for the number of iterations. */
 static int count = 0;
 
diff --git a/test/cbmc/proofs/Posix_OtaSendEvent/Posix_OtaSendEvent_harness.c b/test/cbmc/proofs/Posix_OtaSendEvent/Posix_OtaSendEvent_harness.c
@@ -34,6 +34,8 @@
 /* Counter for the number of iterations. */
 static int count = 0;
 
+int nondet_int();
+
 int poll( struct pollfd * fds,
           nfds_t nfds,
           int timeout )
diff --git a/test/cbmc/proofs/closeFileHandler/closeFileHandler_harness.c b/test/cbmc/proofs/closeFileHandler/closeFileHandler_harness.c
@@ -29,6 +29,8 @@
 /*  Ota Agent includes. */
 #include "ota.h"
 
+#include <stdlib.h>
+
 OtaErr_t __CPROVER_file_local_ota_c_closeFileHandler( const OtaEventData_t * pEventData );
 
 void closeFileHandler_harness()
diff --git a/test/cbmc/proofs/decodeBase64IndexBuffer/decodeBase64IndexBuffer_harness.c b/test/cbmc/proofs/decodeBase64IndexBuffer/decodeBase64IndexBuffer_harness.c
@@ -39,11 +39,11 @@
 #define MAX_NUM_BASE64_DATA            4U
 
 /* Declaration of the mangled name static function which is created by CBMC for static functions. */
-Base64Status_t __CPROVER_file_local_ota_base64_c_decodeBase64IndexBuffer( uint8_t * pDest,
-                                                                          const size_t destLen,
-                                                                          size_t * pResultLen,
+Base64Status_t __CPROVER_file_local_ota_base64_c_decodeBase64IndexBuffer( uint32_t * pDest,
+                                                                          uint32_t * destLen,
                                                                           const uint8_t * pEncodedData,
-                                                                          const size_t encodedLen );
+                                                                          const size_t encodedLen,
+                                                                          size_t * pResultLen );
 
 void decodeBase64IndexBuffer_harness()
 {
diff --git a/test/cbmc/proofs/executeHandler/executeHandler_harness.c b/test/cbmc/proofs/executeHandler/executeHandler_harness.c
@@ -29,6 +29,8 @@
 /*  Ota Agent includes. */
 #include "ota.h"
 
+#include <stdlib.h>
+
 void __CPROVER_file_local_ota_c_executeHandler( uint32_t index,
                                                 const OtaEventMsg_t * const pEventMsg );
 
diff --git a/test/cbmc/proofs/extractAndStoreArray/extractAndStoreArray_harness.c b/test/cbmc/proofs/extractAndStoreArray/extractAndStoreArray_harness.c
@@ -32,11 +32,11 @@
 #include <stdlib.h>
 
 extern OtaAgentContext_t otaAgent;
-extern uint32_t extractAndStoreArray( const char * pKey,
-                                      const char * pValueInJson,
-                                      size_t valueLength,
-                                      void * pParamAdd,
-                                      uint32_t * pParamSizeAdd );
+extern DocParseErr_t extractAndStoreArray( const char * pKey,
+                                           const char * pValueInJson,
+                                           size_t valueLength,
+                                           void * pParamAdd,
+                                           uint32_t * pParamSizeAdd );
 
 void extractAndStoreArray_harness()
 {
diff --git a/test/cbmc/proofs/freeFileContextMem/freeFileContextMem_harness.c b/test/cbmc/proofs/freeFileContextMem/freeFileContextMem_harness.c
@@ -34,6 +34,8 @@
 extern OtaAgentContext_t otaAgent;
 extern void freeFileContextMem( OtaFileContext_t * const pFileContext );
 
+__CPROVER_bool nondet_bool();
+
 void freeFileContextMem_harness()
 {
     OtaInterfaces_t otaInterface;
diff --git a/test/cbmc/proofs/getFileContextFromJob/getFileContextFromJob_harness.c b/test/cbmc/proofs/getFileContextFromJob/getFileContextFromJob_harness.c
@@ -40,6 +40,8 @@ static OtaErr_t getFileContextFromJob( const char * pRawMsg,
                                        uint32_t messageLength,
                                        OtaFileContext_t ** pFileContext );
 
+__CPROVER_bool nondet_bool();
+
 DocParseErr_t parseJobDoc( const JsonDocParam_t * pJsonExpectedParams,
                            uint16_t numJobParams,
                            const char * pJson,
@@ -84,7 +86,7 @@ DocParseErr_t parseJobDoc( const JsonDocParam_t * pJsonExpectedParams,
 
 void getFileContextFromJob_harness()
 {
-    OtaFileContext_t * pFileContext;
+    OtaFileContext_t * pFileContext = &fileContext;
     OtaInterfaces_t otaInterface;
     char rawMsg[ OTA_DATA_BLOCK_SIZE ];
     uint32_t messageLength;
@@ -110,5 +112,5 @@ void getFileContextFromJob_harness()
      * Agent specifically in receiveAndProcessOTAEvent function.*/
     otaAgent.pOtaInterface = &otaInterface;
 
-    ( void ) getFileContextFromJob( &rawMsg, messageLength, &fileContext );
+    ( void ) getFileContextFromJob( rawMsg, messageLength, &pFileContext );
 }
diff --git a/test/cbmc/proofs/handleJobParsingError/handleJobParsingError_harness.c b/test/cbmc/proofs/handleJobParsingError/handleJobParsingError_harness.c
@@ -46,7 +46,7 @@ void handleJobParsingError_harness()
     /* handleJobParsingError is only called with otaAgent.fileContext as it's argument.
      * otaAgent.fileContext.pJobName is pointing to a local buffer which is initialized in initializeLocalBuffers
      * function which is again called in OTA_Init.*/
-    fileContext.pJobName = &jobNameBuffer;
+    fileContext.pJobName = jobNameBuffer;
 
     /* Havoc otaAgent to non-deterministically set all the bytes in
      * the structure. */
diff --git a/test/cbmc/proofs/otaClose/otaClose_harness.c b/test/cbmc/proofs/otaClose/otaClose_harness.c
@@ -36,6 +36,8 @@ extern OtaDataInterface_t otaDataInterface;
 extern OtaAgentContext_t otaAgent;
 extern bool otaClose( OtaFileContext_t * const pFileContext );
 
+__CPROVER_bool nondet_bool();
+
 void otaClose_harness()
 {
     OtaFileContext_t * pFileContext;
diff --git a/test/cbmc/proofs/parseJSONbyModel/parseJSONbyModel_harness.c b/test/cbmc/proofs/parseJSONbyModel/parseJSONbyModel_harness.c
@@ -30,6 +30,8 @@
 #include "ota.h"
 #include "core_json.h"
 
+#include <stdlib.h>
+
 extern OtaAgentContext_t otaAgent;
 extern JsonDocParam_t otaJobDocModelParamStructure[ OTA_NUM_JOB_PARAMS ];
 extern DocParseErr_t parseJSONbyModel( const char * pJson,
diff --git a/test/cbmc/proofs/processDataBlock/processDataBlock_harness.c b/test/cbmc/proofs/processDataBlock/processDataBlock_harness.c
@@ -32,11 +32,11 @@
 #include <stdlib.h>
 
 extern OtaAgentContext_t otaAgent;
-extern uint32_t processDataBlock( OtaFileContext_t * pFileContext,
-                                  uint32_t uBlockIndex,
-                                  uint32_t uBlockSize,
-                                  OtaPalStatus_t * pCloseResult,
-                                  uint8_t * pPayload );
+extern IngestResult_t processDataBlock( OtaFileContext_t * pFileContext,
+                                        uint32_t uBlockIndex,
+                                        uint32_t uBlockSize,
+                                        OtaPalStatus_t * pCloseResult,
+                                        uint8_t * pPayload );
 
 /* Stub to validate incoming data block. */
 bool validateDataBlock( const OtaFileContext_t * pFileContext,
diff --git a/test/cbmc/proofs/requestTimerCallback/requestTimerCallback_harness.c b/test/cbmc/proofs/requestTimerCallback/requestTimerCallback_harness.c
@@ -31,6 +31,8 @@
 #include "FreeRTOS.h"
 #include "timers.h"
 
+#include <stdlib.h>
+
 /* Declaration of the mangled name function created by CBMC for static functions.*/
 void __CPROVER_file_local_ota_os_freertos_c_requestTimerCallback( TimerHandle_t timer );
 
diff --git a/test/cbmc/proofs/resetEventQueue/resetEventQueue_harness.c b/test/cbmc/proofs/resetEventQueue/resetEventQueue_harness.c
@@ -30,6 +30,8 @@
 #include "ota.h"
 #include <stdlib.h>
 
+void resetEventQueue( void );
+
 OtaOsStatus_t recv( OtaEventContext_t * pEventCtx,
                     void * pEventMsg,
                     uint32_t timeout )
diff --git a/test/cbmc/proofs/resumeHandler/resumeHandler_harness.c b/test/cbmc/proofs/resumeHandler/resumeHandler_harness.c
@@ -29,6 +29,8 @@
 /*  Ota Agent includes. */
 #include "ota.h"
 
+#include <stdlib.h>
+
 /* Mangled name definition of the static function. */
 OtaErr_t __CPROVER_file_local_ota_c_resumeHandler( const OtaEventData_t * pEventData );
 
diff --git a/test/cbmc/proofs/selfTestTimerCallback/selfTestTimerCallback_harness.c b/test/cbmc/proofs/selfTestTimerCallback/selfTestTimerCallback_harness.c
@@ -31,6 +31,8 @@
 #include "FreeRTOS.h"
 #include "timers.h"
 
+#include <stdlib.h>
+
 /* Declaration of the mangled name function created by CBMC for static functions.*/
 void __CPROVER_file_local_ota_os_freertos_c_selfTestTimerCallback( TimerHandle_t timer );
 
diff --git a/test/cbmc/proofs/shutdownHandler/shutdownHandler_harness.c b/test/cbmc/proofs/shutdownHandler/shutdownHandler_harness.c
@@ -29,6 +29,8 @@
 /*  Ota Agent includes. */
 #include "ota.h"
 
+#include <stdlib.h>
+
 OtaErr_t __CPROVER_file_local_ota_c_shutdownHandler( const OtaEventData_t * pEventData );
 
 void shutdownHandler_harness()
diff --git a/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c b/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c
@@ -28,6 +28,8 @@
  */
 #include "ota_mqtt_private.h"
 
+#include <stdlib.h>
+
 /* Declaration of the mangled name function generated by CBMC for static functions. */
 size_t __CPROVER_file_local_ota_mqtt_c_stringBuilder( char * pBuffer,
                                                       size_t bufferSizeBytes,
diff --git a/test/cbmc/proofs/suspendHandler/suspendHandler_harness.c b/test/cbmc/proofs/suspendHandler/suspendHandler_harness.c
@@ -29,6 +29,8 @@
 /*  Ota Agent includes. */
 #include "ota.h"
 
+#include <stdlib.h>
+
 OtaErr_t __CPROVER_file_local_ota_c_suspendHandler( const OtaEventData_t * pEventData );
 
 void suspendHandler_harness()
diff --git a/test/cbmc/proofs/verifyActiveJobStatus/verifyActiveJobStatus_harness.c b/test/cbmc/proofs/verifyActiveJobStatus/verifyActiveJobStatus_harness.c
@@ -39,6 +39,8 @@ extern OtaJobParseErr_t verifyActiveJobStatus( OtaFileContext_t * pFileContext,
                                                OtaFileContext_t ** pFinalFile,
                                                bool * pUpdateJob );
 
+__CPROVER_bool nondet_bool();
+
 void verifyActiveJobStatus_harness()
 {
     OtaInterfaces_t otaInterface;

Original file line number	Diff line number	Diff line change
`@@ -29,6 +29,8 @@`
`29`	`29`	`/* FreeRTOS includes for OTA library. */`
`30`	`30`	`#include "ota_os_freertos.h"`
`31`	`31`
	`32`	`+#include <stdlib.h>`
	`33`	`+`
`32`	`34`	`void * pvPortMalloc( size_t size )`
`33`	`35`	`{`
`34`	`36`	`return malloc( size );`
Original file line number	Diff line number	Diff line change
`@@ -30,6 +30,8 @@`
`30`	`30`	`#include "cbor.h"`
`31`	`31`	`#include "ota_cbor_private.h"`
`32`	`32`
	`33`	`+#include <stdlib.h>`
	`34`	`+`
`33`	`35`	`/* Stub to return CBORerror type. */`
`34`	`36`	`CborError returnCborError()`
`35`	`37`	`{`