Skip to content

fix CBMC potential issues #70

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

Merged
ActoryOu merged 12 commits into from
Dec 7, 2021
Merged

fix CBMC potential issues #70

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
44e964e
fix cbmc warning
Nov 29, 2021
844368d
revert useless .c files in Makefile
ActoryOu Nov 30, 2021
5bfde81
all verification pass
ActoryOu Dec 1, 2021
298289a
fix snprintf warning
ActoryOu Dec 2, 2021
acaf3d0
Merge remote-tracking branch 'forkBy/main' into main
ActoryOu Dec 3, 2021
7451c45
replace strnlen with memchr
ActoryOu Dec 3, 2021
4ec1f2f
wrap useless input
ActoryOu Dec 3, 2021
ec7c5d5
fix format check
ActoryOu Dec 3, 2021
42951ea
add strstr to avoid spelling check
ActoryOu Dec 3, 2021
7cca5cf
fix 0.69 uncrustify
ActoryOu Dec 3, 2021
bcb35f6
fix CBMC build error
ActoryOu Dec 3, 2021
be0f2c0
remove test scripts
ActoryOu Dec 6, 2021
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
1 change: 1 addition & 0 deletions lexicon.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -774,6 +774,7 @@ stringlength
strlen
strncpy
strnlen
strstr
strtok
strtol
struct
Expand Down
47 changes: 37 additions & 10 deletions test/cbmc/include/cellular_platform.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,8 @@ typedef void * PVOID;
#define PlatformMutex_TryLock MockPlatformMutex_TryLock
#define PlatformMutex_Unlock MockPlatformMutex_Unlock

#define Platform_CreateDetachedThread MockPlatform_CreateDetachedThread

#define taskENTER_CRITICAL() PVOID
#define taskEXIT_CRITICAL() PVOID

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

#if ( configUSE_16_BIT_TICKS == 1 )
typedef uint16_t TickType_t;
#define portMAX_DELAY ( TickType_t ) 0xffff
#else
typedef uint64_t TickType_t;
#define portMAX_DELAY ( TickType_t ) 0xffffffffUL
#endif

/*
* The type that holds event bits always matches TickType_t - therefore the
* number of bits it holds is set by configUSE_16_BIT_TICKS (16 bits if set to 1,
* 32 bits if set to 0.
*
* \defgroup EventBits_t EventBits_t
* \ingroup EventGroup
*/
typedef TickType_t EventBits_t;

/**
* @brief Cellular library platform thread API and configuration.
*
Expand All @@ -107,9 +127,9 @@ typedef void * PVOID;
* the platform related stack size and priority.
*/

bool Platform_CreateDetachedThread( void ( * threadRoutine )( void * ),
bool Platform_CreateDetachedThread( void ( * threadRoutine )( void * pArgument ),
void * pArgument,
int32_t priority,
size_t priority,
size_t stackSize );

#define PLATFORM_THREAD_DEFAULT_STACK_SIZE ( 2048U )
Expand Down Expand Up @@ -180,6 +200,9 @@ void PlatformMutex_Destroy( PlatformMutex_t * pMutex );
void PlatformMutex_Lock( PlatformMutex_t * pMutex );
bool PlatformMutex_TryLock( PlatformMutex_t * pMutex );
void PlatformMutex_Unlock( PlatformMutex_t * pMutex );
int32_t PlatformEventGroup_SetBitsFromISR( PlatformEventGroupHandle_t groupEvent,
EventBits_t event,
BaseType_t * pHigherPriorityTaskWoken );
void * safeMalloc( size_t xWantedSize );
void allocateSocket( void * pCellularHandle );
bool MockxQueueReceive( int32_t * queue,
Expand All @@ -188,6 +211,18 @@ bool MockxQueueReceive( int32_t * queue,
uint16_t MockPlatformEventGroup_Create();
uint16_t MockPlatformEventGroup_WaitBits();

QueueHandle_t xQueueCreate( int32_t uxQueueLength,
uint32_t uxItemSize );
uint16_t vQueueDelete( QueueHandle_t queue );
BaseType_t xQueueSend( QueueHandle_t queue,
void * data,
uint32_t time );

uint16_t PlatformEventGroup_ClearBits( PlatformEventGroupHandle_t xEventGroup,
TickType_t uxBitsToClear );
uint16_t PlatformEventGroup_Delete( PlatformEventGroupHandle_t groupEvent );
uint16_t PlatformEventGroup_GetBits( PlatformEventGroupHandle_t groupEvent );

/*-----------------------------------------------------------*/

/**
Expand All @@ -202,12 +237,4 @@ uint16_t MockPlatformEventGroup_WaitBits();
#define Platform_Malloc safeMalloc
#define Platform_Free free

#if ( configUSE_16_BIT_TICKS == 1 )
typedef uint16_t TickType_t;
#define portMAX_DELAY ( TickType_t ) 0xffff
#else
typedef uint64_t TickType_t;
#define portMAX_DELAY ( TickType_t ) 0xffffffffUL
#endif

#endif /* __CELLULAR_PLATFORM_H__ */
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,11 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)

UNWINDSET += Cellular_ATGetSpecificNextTok.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)

PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strtok.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c


Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,11 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)

UNWINDSET += Cellular_ATHexStrToHex.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)


PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c

include ../Makefile.common
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_ATIsPrefixPresent/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,12 +35,14 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)
UNWINDSET += Cellular_ATIsPrefixPresent.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += strchr.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += strnlen.0:$(CBMC_MAX_BUFSIZE)


PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strchr.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strnlen.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c

include ../Makefile.common
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,11 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)

UNWINDSET += Cellular_ATIsStrDigit.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)


PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c

include ../Makefile.common
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,11 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)

UNWINDSET += Cellular_ATRemoveAllDoubleQuote.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)


PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c

include ../Makefile.common
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,11 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)

UNWINDSET += Cellular_ATRemoveAllWhiteSpaces.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)


PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c

include ../Makefile.common
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,11 +33,13 @@ CBMC_MAX_BUFSIZE=128
DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)

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


PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c

include ../Makefile.common
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,11 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)

UNWINDSET += Cellular_ATRemoveOutermostDoubleQuote.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)


PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c

include ../Makefile.common
4 changes: 4 additions & 0 deletions test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,13 +30,17 @@ INCLUDES +=
# without tripping unwinding assertions and without exhausting memory.
CBMC_MAX_BUFSIZE=256

DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)

UNWINDSET += strchr.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)


PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strchr.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c

include ../Makefile.common
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,11 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)

UNWINDSET += Cellular_ATRemoveTrailingWhiteSpaces.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)


PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c

include ../Makefile.common
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_ATStrDup/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,11 +34,13 @@ DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)

UNWINDSET += Cellular_ATStrDup.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += strlen.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)

PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strtok.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c


Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_ATStrStartWith/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,12 +33,14 @@ CBMC_MAX_BUFSIZE=256
DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)

UNWINDSET += Cellular_ATStrStartWith.0:$(CBMC_MAX_BUFSIZE)
UNWINDSET += memchr.0:$(CBMC_MAX_BUFSIZE)


PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strchr.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c

include ../Makefile.common
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_ATStrtoi/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,10 +33,12 @@ CBMC_MAX_BUFSIZE=32
DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)

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

PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memchr.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_at_core.c
PROJECT_SOURCES += $(SRCDIR)/test/cbmc/stubs/strtol.c

Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ KEY_LIST_SIZE=16
DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) -DKEY_LIST_SIZE=$(KEY_LIST_SIZE)

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

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

include ../Makefile.common
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_CommonATCommandRaw/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,8 @@ INCLUDES +=
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources//cellular_platform.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources//cellular_modules.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c

Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_CommonCleanup/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,8 @@ UNWINDSET += __CPROVER_file_local_cellular_common_c__Cellular_FreeContext.0:$(CB
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c

Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,8 @@ UNWINDSET += harness.0:$(CBMC_MAX_BUFSIZE)
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c

Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_CommonGetEidrxSettings/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,8 @@ INCLUDES +=
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c
Expand Down
3 changes: 3 additions & 0 deletions test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,9 @@ INCLUDES +=
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/snprintf.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_CommonGetModemInfo/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,8 @@ INCLUDES +=

PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_CommonGetNetworkTime/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,8 @@ INCLUDES +=
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_CommonGetPsmSettings/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,8 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_CommonGetRegisteredNetwork/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,8 @@ INCLUDES +=
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_CommonGetServiceStatus/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,8 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c
Expand Down
2 changes: 2 additions & 0 deletions test/cbmc/proofs/Cellular_CommonGetSimCardInfo/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,8 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/global_state_cellular.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/strncpy.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c
Expand Down
Loading