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 <[email protected]>
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

‎test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,13 +30,17 @@ INCLUDES +=
3030
# without tripping unwinding assertions and without exhausting memory.
3131
CBMC_MAX_BUFSIZE=256
3232

33+
DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)
34+
3335
UNWINDSET += strchr.0:$(CBMC_MAX_BUFSIZE)
36+
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)
3437

3538

3639
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
3740
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
3841
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
3942
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strchr.c
43+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
4044
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c
4145

4246
include ../Makefile.common

‎test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/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_ATRemoveTrailingWhiteSpaces.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_ATStrDup/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_ATStrDup.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_ATStrStartWith/Makefile

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

3535
UNWINDSET += Cellular_ATStrStartWith.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
4142
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strchr.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_ATStrtoi/Makefile

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

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

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

‎test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ KEY_LIST_SIZE=16
3535
DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) -DKEY_LIST_SIZE=$(KEY_LIST_SIZE)
3636

3737
UNWINDSET += Cellular_ATcheckErrorCode.0:$(CBMC_MAX_BUFSIZE)
38+
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)
3839

3940
# This API has its own CBMC test case.
4041
REMOVE_FUNCTION_BODY += Cellular_ATStrStartWith
@@ -43,6 +44,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
4344
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
4445
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
4546
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strchr.c
47+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
4648
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c
4749

4850
include ../Makefile.common

‎test/cbmc/proofs/Cellular_CommonATCommandRaw/Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,8 @@ INCLUDES +=
3030
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
3131
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
3232
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
33+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources//cellular_platform.c
34+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources//cellular_modules.c
3335
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
3436
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
3537

‎test/cbmc/proofs/Cellular_CommonCleanup/Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,8 @@ UNWINDSET += __CPROVER_file_local_cellular_common_c__Cellular_FreeContext.0:$(CB
3838
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
3939
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
4040
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
41+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
42+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
4143
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
4244
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
4345

‎test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,8 @@ UNWINDSET += harness.0:$(CBMC_MAX_BUFSIZE)
4141
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
4242
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
4343
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
44+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
45+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
4446
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
4547
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
4648

‎test/cbmc/proofs/Cellular_CommonGetEidrxSettings/Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,8 @@ INCLUDES +=
3030
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
3131
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
3232
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
33+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
34+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
3335
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
3436
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
3537
PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c

‎test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,9 @@ INCLUDES +=
3030
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
3131
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
3232
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
33+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
34+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
35+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/snprintf.c
3336
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
3437
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
3538
PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c

‎test/cbmc/proofs/Cellular_CommonGetModemInfo/Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,8 @@ INCLUDES +=
2929

3030
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
3131
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
32+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
33+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
3234
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
3335
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
3436
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c

‎test/cbmc/proofs/Cellular_CommonGetNetworkTime/Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,8 @@ INCLUDES +=
3030
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
3131
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
3232
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
33+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
34+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
3335
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
3436
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
3537
PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c

‎test/cbmc/proofs/Cellular_CommonGetPsmSettings/Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,8 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
3131
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
3232
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
3333
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c
34+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
35+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
3436
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
3537
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
3638
PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c

‎test/cbmc/proofs/Cellular_CommonGetRegisteredNetwork/Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,8 @@ INCLUDES +=
3030
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
3131
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
3232
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
33+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
34+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
3335
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
3436
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
3537
PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c

‎test/cbmc/proofs/Cellular_CommonGetServiceStatus/Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,8 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
3131
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
3232
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
3333
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c
34+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
35+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
3436
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
3537
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
3638
PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c

‎test/cbmc/proofs/Cellular_CommonGetSimCardInfo/Makefile

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,8 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
3131
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
3232
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
3333
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c
34+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
35+
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
3436
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
3537
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
3638
PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c

0 commit comments

Comments
 (0)