CBMC proof harness type fixes

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.
aws · Apr 15, 2024 · 8fc7582 · 8fc7582
1 parent 2557f84
commit 8fc7582
Show file tree

Hide file tree

Showing 25 changed files with 59 additions and 18 deletions.
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/...A_CBOR_Decode_GetStreamResponseMessage/OTA_CBOR_Decode_GetStreamResponseMessage_harness.c b/...A_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;