Skip to content

Commit 9583d0d

Browse files
ActoryOuActoryOu
authored
fix CBMC potential issues (#70)
* Remove redundant condition in CBMC stubs * Add more modules/platforms wrappers for CBMC * Fix some CBMC warnings: "WARNING: no body for function" Co-authored-by: Actory Ou <ousc@amazon.com>
1 parent ec48f06 commit 9583d0d

File tree

70 files changed

+681
-17
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

70 files changed

+681
-17
lines changed

‎lexicon.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -774,6 +774,7 @@ stringlength
774774
strlen
775775
strncpy
776776
strnlen
777+
strstr
777778
strtok
778779
strtol
779780
struct

‎test/cbmc/include/cellular_platform.h‎

Lines changed: 37 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,8 @@ typedef void * PVOID;
7575
#define PlatformMutex_TryLock MockPlatformMutex_TryLock
7676
#define PlatformMutex_Unlock MockPlatformMutex_Unlock
7777

78+
#define Platform_CreateDetachedThread MockPlatform_CreateDetachedThread
79+
7880
#define taskENTER_CRITICAL() PVOID
7981
#define taskEXIT_CRITICAL() PVOID
8082

@@ -97,6 +99,24 @@ typedef void * PVOID;
9799
#define CELLULAR_URC_TOKEN_WO_PREFIX_TABLE_SIZE ( sizeof( CellularUrcTokenWoPrefixTable ) / sizeof( char * ) )
98100
#define CELLULAR_SRC_EXTRA_TOKEN_SUCCESS_TABLE_SIZE ( sizeof( CellularSrcExtraTokenSuccessTable ) / sizeof( char * ) )
99101

102+
#if ( configUSE_16_BIT_TICKS == 1 )
103+
typedef uint16_t TickType_t;
104+
#define portMAX_DELAY ( TickType_t ) 0xffff
105+
#else
106+
typedef uint64_t TickType_t;
107+
#define portMAX_DELAY ( TickType_t ) 0xffffffffUL
108+
#endif
109+
110+
/*
111+
* The type that holds event bits always matches TickType_t - therefore the
112+
* number of bits it holds is set by configUSE_16_BIT_TICKS (16 bits if set to 1,
113+
* 32 bits if set to 0.
114+
*
115+
* \defgroup EventBits_t EventBits_t
116+
* \ingroup EventGroup
117+
*/
118+
typedef TickType_t EventBits_t;
119+
100120
/**
101121
* @brief Cellular library platform thread API and configuration.
102122
*
@@ -107,9 +127,9 @@ typedef void * PVOID;
107127
* the platform related stack size and priority.
108128
*/
109129

110-
bool Platform_CreateDetachedThread( void ( * threadRoutine )( void * ),
130+
bool Platform_CreateDetachedThread( void ( * threadRoutine )( void * pArgument ),
111131
void * pArgument,
112-
int32_t priority,
132+
size_t priority,
113133
size_t stackSize );
114134

115135
#define PLATFORM_THREAD_DEFAULT_STACK_SIZE ( 2048U )
@@ -180,6 +200,9 @@ void PlatformMutex_Destroy( PlatformMutex_t * pMutex );
180200
void PlatformMutex_Lock( PlatformMutex_t * pMutex );
181201
bool PlatformMutex_TryLock( PlatformMutex_t * pMutex );
182202
void PlatformMutex_Unlock( PlatformMutex_t * pMutex );
203+
int32_t PlatformEventGroup_SetBitsFromISR( PlatformEventGroupHandle_t groupEvent,
204+
EventBits_t event,
205+
BaseType_t * pHigherPriorityTaskWoken );
183206
void * safeMalloc( size_t xWantedSize );
184207
void allocateSocket( void * pCellularHandle );
185208
bool MockxQueueReceive( int32_t * queue,
@@ -188,6 +211,18 @@ bool MockxQueueReceive( int32_t * queue,
188211
uint16_t MockPlatformEventGroup_Create();
189212
uint16_t MockPlatformEventGroup_WaitBits();
190213

214+
QueueHandle_t xQueueCreate( int32_t uxQueueLength,
215+
uint32_t uxItemSize );
216+
uint16_t vQueueDelete( QueueHandle_t queue );
217+
BaseType_t xQueueSend( QueueHandle_t queue,
218+
void * data,
219+
uint32_t time );
220+
221+
uint16_t PlatformEventGroup_ClearBits( PlatformEventGroupHandle_t xEventGroup,
222+
TickType_t uxBitsToClear );
223+
uint16_t PlatformEventGroup_Delete( PlatformEventGroupHandle_t groupEvent );
224+
uint16_t PlatformEventGroup_GetBits( PlatformEventGroupHandle_t groupEvent );
225+
191226
/*-----------------------------------------------------------*/
192227

193228
/**
@@ -202,12 +237,4 @@ uint16_t MockPlatformEventGroup_WaitBits();
202237
#define Platform_Malloc safeMalloc
203238
#define Platform_Free free
204239

205-
#if ( configUSE_16_BIT_TICKS == 1 )
206-
typedef uint16_t TickType_t;
207-
#define portMAX_DELAY ( TickType_t ) 0xffff
208-
#else
209-
typedef uint64_t TickType_t;
210-
#define portMAX_DELAY ( TickType_t ) 0xffffffffUL
211-
#endif
212-
213240
#endif /* __CELLULAR_PLATFORM_H__ */

‎test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,11 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)
3434

3535
UNWINDSET += Cellular_ATGetSpecificNextTok.0:$(CBMC_MAX_BUFSIZE)
3636
UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE)
37+
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)
3738

3839
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
3940
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
4041
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
4142
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strtok.c
43+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
4244
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c
4345

4446

‎test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,11 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)
3434

3535
UNWINDSET += Cellular_ATHexStrToHex.0:$(CBMC_MAX_BUFSIZE)
3636
UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE)
37+
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)
3738

3839

3940
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
4041
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
4142
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
43+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
4244
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c
4345

4446
include ../Makefile.common

‎test/cbmc/proofs/Cellular_ATIsPrefixPresent/Makefile‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,12 +35,14 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)
3535
UNWINDSET += Cellular_ATIsPrefixPresent.0:$(CBMC_MAX_BUFSIZE)
3636
UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE)
3737
UNWINDSET += strchr.0:$(CBMC_MAX_BUFSIZE)
38+
UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE)
3839

3940

4041
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
4142
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
4243
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
4344
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strchr.c
45+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c
4446
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c
4547

4648
include ../Makefile.common

‎test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,11 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)
3434

3535
UNWINDSET += Cellular_ATIsStrDigit.0:$(CBMC_MAX_BUFSIZE)
3636
UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE)
37+
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)
3738

3839

3940
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
4041
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
4142
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
43+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
4244
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c
4345

4446
include ../Makefile.common

‎test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,11 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)
3434

3535
UNWINDSET += Cellular_ATRemoveAllDoubleQuote.0:$(CBMC_MAX_BUFSIZE)
3636
UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE)
37+
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)
3738

3839

3940
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
4041
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
4142
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
43+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
4244
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c
4345

4446
include ../Makefile.common

‎test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,11 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)
3434

3535
UNWINDSET += Cellular_ATRemoveAllWhiteSpaces.0:$(CBMC_MAX_BUFSIZE)
3636
UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE)
37+
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)
3738

3839

3940
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
4041
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
4142
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
43+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
4244
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c
4345

4446
include ../Makefile.common

‎test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,11 +33,13 @@ CBMC_MAX_BUFSIZE=128
3333
DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)
3434

3535
UNWINDSET += Cellular_ATRemoveLeadingWhiteSpaces.0:$(CBMC_MAX_BUFSIZE)
36+
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)
3637

3738

3839
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
3940
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
4041
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
42+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
4143
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c
4244

4345
include ../Makefile.common

‎test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,11 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)
3434

3535
UNWINDSET += Cellular_ATRemoveOutermostDoubleQuote.0:$(CBMC_MAX_BUFSIZE)
3636
UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE)
37+
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)
3738

3839

3940
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
4041
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
4142
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
43+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
4244
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c
4345

4446
include ../Makefile.common

0 commit comments

Comments
 (0)