Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

CBMC proof harness type fixes #510

Merged
merged 1 commit into from
Apr 17, 2024
Merged

CBMC proof harness type fixes #510

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Malloc_FreeRTOS/Malloc_FreeRTOS_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,8 @@
/* FreeRTOS includes for OTA library. */
#include "ota_os_freertos.h"

#include <stdlib.h>
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

NIT: should we not include such standard libs before the headers of our own libraries as a rule of FreeRTOS?

Copy link
Contributor Author

@tautschnig tautschnig Apr 15, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Happy to adjust this if there is such a rule, I wasn't aware. Edit: none of the other harnesses seem to be following this, so I haven't changed it for now. Please let me know if you'd like me to change it.


void * pvPortMalloc( size_t size )
{
return malloc( size );
Expand Down
2 changes: 2 additions & 0 deletions ...A_CBOR_Decode_GetStreamResponseMessage/OTA_CBOR_Decode_GetStreamResponseMessage_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,8 @@
#include "cbor.h"
#include "ota_cbor_private.h"

#include <stdlib.h>

/* Stub to return CBORerror type. */
CborError returnCborError()
{
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/OTA_GetStatistics/OTA_GetStatistics_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,8 @@
/* Ota Agent includes. */
#include "ota.h"

#include <stdlib.h>

void OTA_GetStatistics_harness()
{
OtaErr_t err;
Expand Down
3 changes: 2 additions & 1 deletion test/cbmc/proofs/OtaReceiveEvent_FreeRTOS/OtaReceiveEvent_FreeRTOS_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ) );
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/OtaStartTimer_FreeRTOS/OtaStartTimer_FreeRTOS_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Posix_OtaReceiveEvent/Posix_OtaReceiveEvent_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,8 @@
#include <poll.h>
#include <mqueue.h>

int nondet_int();
tautschnig marked this conversation as resolved.
Show resolved Hide resolved

/* Counter for the number of iterations. */
static int count = 0;

Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Posix_OtaSendEvent/Posix_OtaSendEvent_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 )
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/closeFileHandler/closeFileHandler_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down
8 changes: 4 additions & 4 deletions test/cbmc/proofs/decodeBase64IndexBuffer/decodeBase64IndexBuffer_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 );
tautschnig marked this conversation as resolved.
Show resolved Hide resolved

void decodeBase64IndexBuffer_harness()
{
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/executeHandler/executeHandler_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 );

Expand Down
10 changes: 5 additions & 5 deletions test/cbmc/proofs/extractAndStoreArray/extractAndStoreArray_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()
{
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/freeFileContextMem/freeFileContextMem_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,8 @@
extern OtaAgentContext_t otaAgent;
extern void freeFileContextMem( OtaFileContext_t * const pFileContext );

__CPROVER_bool nondet_bool();
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why does this need to be declared here? And why the special return type given the earlier example nondet_int was returning a standard type?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here, this is only used for a true/false decision. We could, however, also pick a different type (that can be converted to an int) in here.


void freeFileContextMem_harness()
{
OtaInterfaces_t otaInterface;
Expand Down
6 changes: 4 additions & 2 deletions test/cbmc/proofs/getFileContextFromJob/getFileContextFromJob_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -84,7 +86,7 @@ DocParseErr_t parseJobDoc( const JsonDocParam_t * pJsonExpectedParams,

void getFileContextFromJob_harness()
{
OtaFileContext_t * pFileContext;
OtaFileContext_t * pFileContext = &fileContext;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not get rid of this previously unused variable instead of now assigning it a value?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There actually is a good use for this variable, see the next change: it's now used in calling getFileContextFromJob (which was previously passed a variable of the wrong type).

OtaInterfaces_t otaInterface;
char rawMsg[ OTA_DATA_BLOCK_SIZE ];
uint32_t messageLength;
Expand All @@ -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 );
}
2 changes: 1 addition & 1 deletion test/cbmc/proofs/handleJobParsingError/handleJobParsingError_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. */
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/otaClose/otaClose_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/parseJSONbyModel/parseJSONbyModel_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
10 changes: 5 additions & 5 deletions test/cbmc/proofs/processDataBlock/processDataBlock_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/requestTimerCallback/requestTimerCallback_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 );

Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/resetEventQueue/resetEventQueue_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,8 @@
#include "ota.h"
#include <stdlib.h>

void resetEventQueue( void );

OtaOsStatus_t recv( OtaEventContext_t * pEventCtx,
void * pEventMsg,
uint32_t timeout )
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/resumeHandler/resumeHandler_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 );

Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/selfTestTimerCallback/selfTestTimerCallback_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 );

Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/shutdownHandler/shutdownHandler_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/stringBuilder/stringBuilder_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/suspendHandler/suspendHandler_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/verifyActiveJobStatus/verifyActiveJobStatus_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
Loading