diff --git a/lexicon.txt b/lexicon.txt
index b4572209..64462cad 100644
--- a/lexicon.txt
+++ b/lexicon.txt
@@ -774,6 +774,7 @@ stringlength
 strlen
 strncpy
 strnlen
+strstr
 strtok
 strtol
 struct
diff --git a/test/cbmc/include/cellular_platform.h b/test/cbmc/include/cellular_platform.h
index 7e9e4ca3..7b620c57 100644
--- a/test/cbmc/include/cellular_platform.h
+++ b/test/cbmc/include/cellular_platform.h
@@ -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
 
@@ -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.
  *
@@ -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 )
@@ -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,
@@ -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 );
+
 /*-----------------------------------------------------------*/
 
 /**
@@ -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__ */
diff --git a/test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile b/test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile
index 93959ec1..ac03fc07 100755
--- a/test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile
+++ b/test/cbmc/proofs/Cellular_ATGetSpecificNextTok/Makefile
@@ -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
 
 
diff --git a/test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile b/test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile
index 6d823f7a..cf369c9e 100755
--- a/test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile
+++ b/test/cbmc/proofs/Cellular_ATHexStrToHex/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_ATIsPrefixPresent/Makefile b/test/cbmc/proofs/Cellular_ATIsPrefixPresent/Makefile
index a9282ce5..e1bafa2b 100755
--- a/test/cbmc/proofs/Cellular_ATIsPrefixPresent/Makefile
+++ b/test/cbmc/proofs/Cellular_ATIsPrefixPresent/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile b/test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile
index 69f5f741..65c33ba4 100755
--- a/test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile
+++ b/test/cbmc/proofs/Cellular_ATIsStrDigit/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile b/test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile
index d5dbc6cc..dfaaad08 100755
--- a/test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile
+++ b/test/cbmc/proofs/Cellular_ATRemoveAllDoubleQuote/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile b/test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile
index 2b966431..4bf70091 100755
--- a/test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile
+++ b/test/cbmc/proofs/Cellular_ATRemoveAllWhiteSpaces/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile b/test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile
index ae467499..3a712570 100755
--- a/test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile
+++ b/test/cbmc/proofs/Cellular_ATRemoveLeadingWhiteSpaces/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile b/test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile
index c328ff3a..3c785b20 100755
--- a/test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile
+++ b/test/cbmc/proofs/Cellular_ATRemoveOutermostDoubleQuote/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile b/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile
index 6d9aa7ea..98520cf2 100755
--- a/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile
+++ b/test/cbmc/proofs/Cellular_ATRemovePrefix/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile b/test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile
index c7f586a5..92c1b24d 100755
--- a/test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile
+++ b/test/cbmc/proofs/Cellular_ATRemoveTrailingWhiteSpaces/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_ATStrDup/Makefile b/test/cbmc/proofs/Cellular_ATStrDup/Makefile
index 91398d3e..fa235f45 100755
--- a/test/cbmc/proofs/Cellular_ATStrDup/Makefile
+++ b/test/cbmc/proofs/Cellular_ATStrDup/Makefile
@@ -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
 
 
diff --git a/test/cbmc/proofs/Cellular_ATStrStartWith/Makefile b/test/cbmc/proofs/Cellular_ATStrStartWith/Makefile
index 708d6539..8eedfc7d 100755
--- a/test/cbmc/proofs/Cellular_ATStrStartWith/Makefile
+++ b/test/cbmc/proofs/Cellular_ATStrStartWith/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_ATStrtoi/Makefile b/test/cbmc/proofs/Cellular_ATStrtoi/Makefile
index 9bbf9a2f..82bbd7c7 100755
--- a/test/cbmc/proofs/Cellular_ATStrtoi/Makefile
+++ b/test/cbmc/proofs/Cellular_ATStrtoi/Makefile
@@ -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
 
diff --git a/test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile b/test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile
index 70f7bf11..bb327fe0 100755
--- a/test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile
+++ b/test/cbmc/proofs/Cellular_ATcheckErrorCode/Makefile
@@ -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
@@ -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
diff --git a/test/cbmc/proofs/Cellular_CommonATCommandRaw/Makefile b/test/cbmc/proofs/Cellular_CommonATCommandRaw/Makefile
index 9bf6c0f5..73cb36f5 100755
--- a/test/cbmc/proofs/Cellular_CommonATCommandRaw/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonATCommandRaw/Makefile
@@ -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
 
diff --git a/test/cbmc/proofs/Cellular_CommonCleanup/Makefile b/test/cbmc/proofs/Cellular_CommonCleanup/Makefile
index d0408b20..d4849ef0 100755
--- a/test/cbmc/proofs/Cellular_CommonCleanup/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonCleanup/Makefile
@@ -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
 
diff --git a/test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile b/test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile
index d2b47bb6..a436623d 100755
--- a/test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonCreateSocket/Makefile
@@ -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
 
diff --git a/test/cbmc/proofs/Cellular_CommonGetEidrxSettings/Makefile b/test/cbmc/proofs/Cellular_CommonGetEidrxSettings/Makefile
index 2e492525..d0d272a6 100755
--- a/test/cbmc/proofs/Cellular_CommonGetEidrxSettings/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonGetEidrxSettings/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile b/test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile
index 64e1567f..c5d33ae1 100755
--- a/test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonGetIPAddress/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_CommonGetModemInfo/Makefile b/test/cbmc/proofs/Cellular_CommonGetModemInfo/Makefile
index f46b10c2..b011ab25 100755
--- a/test/cbmc/proofs/Cellular_CommonGetModemInfo/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonGetModemInfo/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_CommonGetNetworkTime/Makefile b/test/cbmc/proofs/Cellular_CommonGetNetworkTime/Makefile
index 6aeeaf33..5084547b 100755
--- a/test/cbmc/proofs/Cellular_CommonGetNetworkTime/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonGetNetworkTime/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_CommonGetPsmSettings/Makefile b/test/cbmc/proofs/Cellular_CommonGetPsmSettings/Makefile
index 1e44b0d8..71b9e780 100755
--- a/test/cbmc/proofs/Cellular_CommonGetPsmSettings/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonGetPsmSettings/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_CommonGetRegisteredNetwork/Makefile b/test/cbmc/proofs/Cellular_CommonGetRegisteredNetwork/Makefile
index 45fb8c17..a3a562be 100755
--- a/test/cbmc/proofs/Cellular_CommonGetRegisteredNetwork/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonGetRegisteredNetwork/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_CommonGetServiceStatus/Makefile b/test/cbmc/proofs/Cellular_CommonGetServiceStatus/Makefile
index 93ef185a..ead1c4e2 100755
--- a/test/cbmc/proofs/Cellular_CommonGetServiceStatus/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonGetServiceStatus/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_CommonGetSimCardInfo/Makefile b/test/cbmc/proofs/Cellular_CommonGetSimCardInfo/Makefile
index abb47096..e504c6b8 100755
--- a/test/cbmc/proofs/Cellular_CommonGetSimCardInfo/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonGetSimCardInfo/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_CommonGetSimCardLockStatus/Makefile b/test/cbmc/proofs/Cellular_CommonGetSimCardLockStatus/Makefile
index aeb1d61e..175a6594 100755
--- a/test/cbmc/proofs/Cellular_CommonGetSimCardLockStatus/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonGetSimCardLockStatus/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_CommonInit/Makefile b/test/cbmc/proofs/Cellular_CommonInit/Makefile
index e6271632..956dd779 100755
--- a/test/cbmc/proofs/Cellular_CommonInit/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonInit/Makefile
@@ -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
 
diff --git a/test/cbmc/proofs/Cellular_CommonRegisterModemEventCallback/Makefile b/test/cbmc/proofs/Cellular_CommonRegisterModemEventCallback/Makefile
index c4f68f14..fd2d13c7 100755
--- a/test/cbmc/proofs/Cellular_CommonRegisterModemEventCallback/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonRegisterModemEventCallback/Makefile
@@ -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_urc_handler.c
diff --git a/test/cbmc/proofs/Cellular_CommonRegisterUrcGenericCallback/Makefile b/test/cbmc/proofs/Cellular_CommonRegisterUrcGenericCallback/Makefile
index 0f981a0e..490b9d8b 100755
--- a/test/cbmc/proofs/Cellular_CommonRegisterUrcGenericCallback/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonRegisterUrcGenericCallback/Makefile
@@ -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_urc_handler.c
diff --git a/test/cbmc/proofs/Cellular_CommonRegisterUrcNetworkRegistrationEventCallback/Makefile b/test/cbmc/proofs/Cellular_CommonRegisterUrcNetworkRegistrationEventCallback/Makefile
index d889c675..082e9fe5 100755
--- a/test/cbmc/proofs/Cellular_CommonRegisterUrcNetworkRegistrationEventCallback/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonRegisterUrcNetworkRegistrationEventCallback/Makefile
@@ -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_urc_handler.c
diff --git a/test/cbmc/proofs/Cellular_CommonRegisterUrcPdnEventCallback/Makefile b/test/cbmc/proofs/Cellular_CommonRegisterUrcPdnEventCallback/Makefile
index a91087d0..41368897 100755
--- a/test/cbmc/proofs/Cellular_CommonRegisterUrcPdnEventCallback/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonRegisterUrcPdnEventCallback/Makefile
@@ -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_urc_handler.c
diff --git a/test/cbmc/proofs/Cellular_CommonRegisterUrcSignalStrengthChangedCallback/Makefile b/test/cbmc/proofs/Cellular_CommonRegisterUrcSignalStrengthChangedCallback/Makefile
index d0ec43a5..1930c260 100755
--- a/test/cbmc/proofs/Cellular_CommonRegisterUrcSignalStrengthChangedCallback/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonRegisterUrcSignalStrengthChangedCallback/Makefile
@@ -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_urc_handler.c
diff --git a/test/cbmc/proofs/Cellular_CommonRfOff/Makefile b/test/cbmc/proofs/Cellular_CommonRfOff/Makefile
index a8a8b3e8..66429427 100755
--- a/test/cbmc/proofs/Cellular_CommonRfOff/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonRfOff/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_CommonRfOn/Makefile b/test/cbmc/proofs/Cellular_CommonRfOn/Makefile
index 17c1038b..29c950c6 100755
--- a/test/cbmc/proofs/Cellular_CommonRfOn/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonRfOn/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_CommonSetEidrxSettings/Makefile b/test/cbmc/proofs/Cellular_CommonSetEidrxSettings/Makefile
index 613b5b1d..54401a96 100755
--- a/test/cbmc/proofs/Cellular_CommonSetEidrxSettings/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonSetEidrxSettings/Makefile
@@ -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
diff --git a/test/cbmc/proofs/Cellular_CommonSetPdnConfig/Makefile b/test/cbmc/proofs/Cellular_CommonSetPdnConfig/Makefile
index b2e25749..2e224e29 100755
--- a/test/cbmc/proofs/Cellular_CommonSetPdnConfig/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonSetPdnConfig/Makefile
@@ -31,6 +31,9 @@ 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/stubs/snprintf.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
diff --git a/test/cbmc/proofs/Cellular_CommonSetPsmSettings/Makefile b/test/cbmc/proofs/Cellular_CommonSetPsmSettings/Makefile
index dc2a955c..cb7c34a2 100755
--- a/test/cbmc/proofs/Cellular_CommonSetPsmSettings/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonSetPsmSettings/Makefile
@@ -31,6 +31,9 @@ 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/stubs/snprintf.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
diff --git a/test/cbmc/proofs/Cellular_CommonSocketRegisterClosedCallback/Makefile b/test/cbmc/proofs/Cellular_CommonSocketRegisterClosedCallback/Makefile
index a6967772..37a23512 100755
--- a/test/cbmc/proofs/Cellular_CommonSocketRegisterClosedCallback/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonSocketRegisterClosedCallback/Makefile
@@ -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_urc_handler.c
diff --git a/test/cbmc/proofs/Cellular_CommonSocketRegisterDataReadyCallback/Makefile b/test/cbmc/proofs/Cellular_CommonSocketRegisterDataReadyCallback/Makefile
index 310cc86b..0e940312 100755
--- a/test/cbmc/proofs/Cellular_CommonSocketRegisterDataReadyCallback/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonSocketRegisterDataReadyCallback/Makefile
@@ -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_urc_handler.c
diff --git a/test/cbmc/proofs/Cellular_CommonSocketRegisterSocketOpenCallback/Makefile b/test/cbmc/proofs/Cellular_CommonSocketRegisterSocketOpenCallback/Makefile
index 9af13958..e7ade9bb 100755
--- a/test/cbmc/proofs/Cellular_CommonSocketRegisterSocketOpenCallback/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonSocketRegisterSocketOpenCallback/Makefile
@@ -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_urc_handler.c
diff --git a/test/cbmc/proofs/Cellular_CommonSocketSetSockOpt/Makefile b/test/cbmc/proofs/Cellular_CommonSocketSetSockOpt/Makefile
index 331c9dd1..47699524 100755
--- a/test/cbmc/proofs/Cellular_CommonSocketSetSockOpt/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonSocketSetSockOpt/Makefile
@@ -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
 
diff --git a/test/cbmc/proofs/Cellular_CommonUrcProcessCereg/Makefile b/test/cbmc/proofs/Cellular_CommonUrcProcessCereg/Makefile
index e615b096..4ff2b620 100755
--- a/test/cbmc/proofs/Cellular_CommonUrcProcessCereg/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonUrcProcessCereg/Makefile
@@ -48,6 +48,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_urc_handler.c
diff --git a/test/cbmc/proofs/Cellular_CommonUrcProcessCgreg/Makefile b/test/cbmc/proofs/Cellular_CommonUrcProcessCgreg/Makefile
index c5750747..8665f417 100755
--- a/test/cbmc/proofs/Cellular_CommonUrcProcessCgreg/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonUrcProcessCgreg/Makefile
@@ -48,6 +48,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_urc_handler.c
diff --git a/test/cbmc/proofs/Cellular_CommonUrcProcessCreg/Makefile b/test/cbmc/proofs/Cellular_CommonUrcProcessCreg/Makefile
index c3035a17..09a28aff 100755
--- a/test/cbmc/proofs/Cellular_CommonUrcProcessCreg/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonUrcProcessCreg/Makefile
@@ -40,6 +40,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_urc_handler.c
diff --git a/test/cbmc/proofs/_Cellular_GenericCallback/Makefile b/test/cbmc/proofs/_Cellular_GenericCallback/Makefile
index f55898fc..6f9f6b4a 100755
--- a/test/cbmc/proofs/_Cellular_GenericCallback/Makefile
+++ b/test/cbmc/proofs/_Cellular_GenericCallback/Makefile
@@ -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_urc_handler.c
diff --git a/test/cbmc/proofs/_Cellular_GetCurrentRat/Makefile b/test/cbmc/proofs/_Cellular_GetCurrentRat/Makefile
index b8f3897a..391cb389 100755
--- a/test/cbmc/proofs/_Cellular_GetCurrentRat/Makefile
+++ b/test/cbmc/proofs/_Cellular_GetCurrentRat/Makefile
@@ -30,6 +30,7 @@ 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
 PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
 PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
 
diff --git a/test/cbmc/proofs/_Cellular_GetModuleContext/Makefile b/test/cbmc/proofs/_Cellular_GetModuleContext/Makefile
index 05e29115..cb8c66cc 100755
--- a/test/cbmc/proofs/_Cellular_GetModuleContext/Makefile
+++ b/test/cbmc/proofs/_Cellular_GetModuleContext/Makefile
@@ -40,6 +40,8 @@ UNWINDSET += _Cellular_CreateSocketData.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
 
diff --git a/test/cbmc/proofs/_Cellular_GetSocketData/Makefile b/test/cbmc/proofs/_Cellular_GetSocketData/Makefile
index 33dc0c49..32b7b90e 100755
--- a/test/cbmc/proofs/_Cellular_GetSocketData/Makefile
+++ b/test/cbmc/proofs/_Cellular_GetSocketData/Makefile
@@ -38,6 +38,8 @@ UNWINDSET += allocateSocket.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
 PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c
diff --git a/test/cbmc/proofs/_Cellular_IsValidSocket/Makefile b/test/cbmc/proofs/_Cellular_IsValidSocket/Makefile
index a58e83f9..dcdbd640 100755
--- a/test/cbmc/proofs/_Cellular_IsValidSocket/Makefile
+++ b/test/cbmc/proofs/_Cellular_IsValidSocket/Makefile
@@ -40,6 +40,8 @@ UNWINDSET += _Cellular_CreateSocketData.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
 
diff --git a/test/cbmc/proofs/_Cellular_IsValidSocket/_Cellular_IsValidSocket_harness.c b/test/cbmc/proofs/_Cellular_IsValidSocket/_Cellular_IsValidSocket_harness.c
index 708059e4..0d7c21c8 100644
--- a/test/cbmc/proofs/_Cellular_IsValidSocket/_Cellular_IsValidSocket_harness.c
+++ b/test/cbmc/proofs/_Cellular_IsValidSocket/_Cellular_IsValidSocket_harness.c
@@ -26,6 +26,7 @@
 #include <stdint.h>
 
 /* Cellular APIs includes. */
+#include "cellular_platform.h"
 #include "cellular_config_defaults.h"
 #include "cellular_types.h"
 #include "cellular_common_internal.h"
diff --git a/test/cbmc/proofs/_Cellular_LibCleanup/Makefile b/test/cbmc/proofs/_Cellular_LibCleanup/Makefile
index eabbcbad..2a98bd73 100755
--- a/test/cbmc/proofs/_Cellular_LibCleanup/Makefile
+++ b/test/cbmc/proofs/_Cellular_LibCleanup/Makefile
@@ -39,6 +39,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_urc_handler.c
diff --git a/test/cbmc/proofs/_Cellular_ModemEventCallback/Makefile b/test/cbmc/proofs/_Cellular_ModemEventCallback/Makefile
index 30e9fe7b..65f93510 100755
--- a/test/cbmc/proofs/_Cellular_ModemEventCallback/Makefile
+++ b/test/cbmc/proofs/_Cellular_ModemEventCallback/Makefile
@@ -39,6 +39,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_urc_handler.c
diff --git a/test/cbmc/proofs/_Cellular_NetworkRegistrationCallback/Makefile b/test/cbmc/proofs/_Cellular_NetworkRegistrationCallback/Makefile
index 3ace40cf..b29481ce 100755
--- a/test/cbmc/proofs/_Cellular_NetworkRegistrationCallback/Makefile
+++ b/test/cbmc/proofs/_Cellular_NetworkRegistrationCallback/Makefile
@@ -39,6 +39,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_urc_handler.c
diff --git a/test/cbmc/proofs/_Cellular_PdnEventCallback/Makefile b/test/cbmc/proofs/_Cellular_PdnEventCallback/Makefile
index 05fe6342..262e6501 100755
--- a/test/cbmc/proofs/_Cellular_PdnEventCallback/Makefile
+++ b/test/cbmc/proofs/_Cellular_PdnEventCallback/Makefile
@@ -39,6 +39,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_urc_handler.c
diff --git a/test/cbmc/proofs/_Cellular_RemoveSocketData/Makefile b/test/cbmc/proofs/_Cellular_RemoveSocketData/Makefile
index ba46854c..f92eee4f 100755
--- a/test/cbmc/proofs/_Cellular_RemoveSocketData/Makefile
+++ b/test/cbmc/proofs/_Cellular_RemoveSocketData/Makefile
@@ -42,6 +42,8 @@ UNWINDSET += _Cellular_RemoveSocketData.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
 
diff --git a/test/cbmc/proofs/_Cellular_SignalStrengthChangedCallback/Makefile b/test/cbmc/proofs/_Cellular_SignalStrengthChangedCallback/Makefile
index 37ab6d5d..0cc3c594 100755
--- a/test/cbmc/proofs/_Cellular_SignalStrengthChangedCallback/Makefile
+++ b/test/cbmc/proofs/_Cellular_SignalStrengthChangedCallback/Makefile
@@ -39,6 +39,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_urc_handler.c
diff --git a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataRecvRequestWithCallback/Makefile b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataRecvRequestWithCallback/Makefile
index 2833c687..30d86fbf 100755
--- a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataRecvRequestWithCallback/Makefile
+++ b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataRecvRequestWithCallback/Makefile
@@ -41,7 +41,7 @@ UNWINDSET += __builtin___strncpy_chk.0:$(CBMC_MAX_BUFSIZE)
 PROJECT_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
-PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
+PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_platform.c
 PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
 PROJECT_SOURCES += $(SRCDIR)/source/cellular_3gpp_api.c
 PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c
diff --git a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendRequestWithCallback/Makefile b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendRequestWithCallback/Makefile
index 9d0b7079..ff8ea82c 100755
--- a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendRequestWithCallback/Makefile
+++ b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendRequestWithCallback/Makefile
@@ -42,6 +42,7 @@ UNWINDSET += __builtin___strncpy_chk.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
 PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
 PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
 PROJECT_SOURCES += $(SRCDIR)/source/cellular_pkthandler.c
diff --git a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendSuccessToken/Makefile b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendSuccessToken/Makefile
index a627efae..8820fe63 100755
--- a/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendSuccessToken/Makefile
+++ b/test/cbmc/proofs/_Cellular_TimeoutAtcmdDataSendSuccessToken/Makefile
@@ -35,6 +35,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
 
diff --git a/test/cbmc/sources/cellular_modules.c b/test/cbmc/sources/cellular_modules.c
new file mode 100644
index 00000000..7fab419a
--- /dev/null
+++ b/test/cbmc/sources/cellular_modules.c
@@ -0,0 +1,71 @@
+/*
+ * FreeRTOS-Cellular-Interface v1.1.0
+ * Copyright (C) 2021 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ */
+
+/**
+ * @file cellular_modules.h
+ * @brief cbmc wrapper functions in cellular_common_portable.h.
+ */
+
+/* Include paths for public enums, structures, and macros. */
+#include "cellular_common_portable.h"
+
+CellularError_t Cellular_ModuleInit( const CellularContext_t * pContext,
+                                     void ** ppModuleContext )
+{
+    CellularError_t ret = nondet_int();
+
+    __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN );
+    return ret;
+}
+
+
+CellularError_t Cellular_ModuleCleanUp( const CellularContext_t * pContext )
+{
+    CellularError_t ret = nondet_int();
+
+    __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN );
+    return ret;
+}
+
+
+CellularError_t Cellular_ModuleEnableUE( CellularContext_t * pContext )
+{
+    CellularError_t ret = nondet_int();
+
+    __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN );
+    return ret;
+}
+
+
+CellularError_t Cellular_ModuleEnableUrc( CellularContext_t * pContext )
+{
+    CellularError_t ret = nondet_int();
+
+    __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN );
+    return ret;
+}
+
+
+/* ========================================================================== */
diff --git a/test/cbmc/sources/cellular_platform.c b/test/cbmc/sources/cellular_platform.c
new file mode 100644
index 00000000..c9e1adb0
--- /dev/null
+++ b/test/cbmc/sources/cellular_platform.c
@@ -0,0 +1,174 @@
+/*
+ * FreeRTOS-Cellular-Interface v1.1.0
+ * Copyright (C) 2021 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ */
+
+/**
+ * @file cellular_platform.c
+ * @brief cbmc wrapper functions in cellular_platform.h.
+ */
+
+/* Include paths for public enums, structures, and macros. */
+#include "cellular_platform.h"
+
+void MockPlatformMutex_Unlock( PlatformMutex_t * pMutex )
+{
+    ( void ) pMutex;
+}
+
+void MockPlatformMutex_Lock( PlatformMutex_t * pMutex )
+{
+    ( void ) pMutex;
+}
+
+void MockPlatformMutex_Destroy( PlatformMutex_t * pMutex )
+{
+    pMutex->created = false;
+}
+
+bool MockPlatformMutex_Create( PlatformMutex_t * pNewMutex,
+                               bool recursive )
+{
+    ( void ) recursive;
+    pNewMutex->created = true;
+    return true;
+}
+
+int32_t MockPlatformEventGroup_SetBitsFromISR( PlatformEventGroupHandle_t groupEvent,
+                                               EventBits_t event,
+                                               BaseType_t * pHigherPriorityTaskWoken )
+{
+    bool flag = nondet_bool();
+    int32_t ret;
+
+    ( void ) groupEvent;
+    ( void ) event;
+    ( void ) pHigherPriorityTaskWoken;
+
+    if( flag )
+    {
+        if( nondet_bool() )
+        {
+            *pHigherPriorityTaskWoken = pdTRUE;
+        }
+        else
+        {
+            *pHigherPriorityTaskWoken = pdFALSE;
+        }
+
+        ret = pdPASS;
+    }
+    else
+    {
+        ret = pdFALSE;
+    }
+
+    return ret;
+}
+
+/* ========================================================================== */
+
+QueueHandle_t MockxQueueCreate( int32_t uxQueueLength,
+                                uint32_t uxItemSize )
+{
+    ( void ) uxQueueLength;
+    ( void ) uxItemSize;
+
+    if( nondet_bool() )
+    {
+        QueueHandle_t test = malloc( sizeof( struct QueueDefinition ) );
+        return test;
+    }
+
+    return NULL;
+}
+
+
+uint16_t MockvQueueDelete( QueueHandle_t queue )
+{
+    free( queue );
+    queue = 0;
+    return 1;
+}
+
+BaseType_t MockxQueueSend( QueueHandle_t queue,
+                           void * data,
+                           uint32_t time )
+{
+    ( void ) queue;
+    ( void ) time;
+
+    if( nondet_bool() )
+    {
+        return true;
+    }
+    else
+    {
+        return false;
+    }
+}
+
+/* ========================================================================== */
+
+
+uint16_t MockPlatformEventGroup_ClearBits( PlatformEventGroupHandle_t xEventGroup,
+                                           TickType_t uxBitsToClear )
+{
+    ( void ) xEventGroup;
+    ( void ) uxBitsToClear;
+    return 0;
+}
+
+bool MockPlatform_CreateDetachedThread( void ( * threadRoutine )( void * pArgument ),
+                                        void * pArgument,
+                                        size_t priority,
+                                        size_t stackSize )
+{
+    ( void ) pArgument;
+    ( void ) priority;
+    ( void ) stackSize;
+
+    bool threadReturn = nondet_bool();
+
+    if( threadReturn )
+    {
+        threadRoutine( pArgument );
+    }
+
+    return threadReturn;
+}
+
+uint16_t MockPlatformEventGroup_Delete( PlatformEventGroupHandle_t groupEvent )
+{
+    ( void ) groupEvent;
+    return 0U;
+}
+
+uint16_t MockPlatformEventGroup_GetBits( PlatformEventGroupHandle_t groupEvent )
+{
+    ( void ) groupEvent;
+
+    uint16_t ret = nondet_unsigned_int();
+
+    return ret;
+}
diff --git a/test/cbmc/stubs/bsearch.c b/test/cbmc/stubs/bsearch.c
new file mode 100644
index 00000000..b3ef36e1
--- /dev/null
+++ b/test/cbmc/stubs/bsearch.c
@@ -0,0 +1,52 @@
+/*
+ * FreeRTOS-Cellular-Interface v1.1.0
+ * Copyright (C) 2021 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ */
+
+/**
+ * @file bsearch.c
+ * @brief Creates a stub for bsearch. This stub checks if, for the input copy
+ * length, the destination and source are valid accessible memory.
+ */
+
+#include <stdio.h>
+
+void * bsearch( const void * key,
+                const void * base,
+                size_t num,
+                size_t size,
+                int ( * compar )( const void *, const void * ) )
+{
+    int offset = nondet_size_t();
+    char * p = ( char * ) base;
+
+    ( void ) key;
+    ( void ) base;
+
+    if( ( offset >= 0 ) && ( offset < num ) )
+    {
+        return ( void * ) ( p + ( offset * size ) );
+    }
+
+    return NULL;
+}
diff --git a/test/cbmc/stubs/memchr.c b/test/cbmc/stubs/memchr.c
new file mode 100644
index 00000000..7a32b99d
--- /dev/null
+++ b/test/cbmc/stubs/memchr.c
@@ -0,0 +1,55 @@
+/*
+ * FreeRTOS-Cellular-Interface v1.1.0
+ * Copyright (C) 2021 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ */
+
+/**
+ * @file strtok.c
+ * @brief Creates a stub for strtok. This stub checks if, for the input copy
+ * length, the destination and source are valid accessible memory.
+ */
+
+#include <stdio.h>
+
+void * memchr( void * ptr,
+               int value,
+               size_t num )
+{
+    /*to avoid unwind assertion on CBMC, use a constant loop time to enhance CBMC performance */
+    int n = CBMC_MAX_BUFSIZE;
+    char * p = ( char * ) ptr;
+
+    ( void ) num;
+
+    while( n-- && p != NULL )
+    {
+        if( *p == ( char ) value )
+        {
+            return p;
+        }
+
+        p++;
+    }
+
+    return NULL;
+}
diff --git a/test/cbmc/stubs/snprintf.c b/test/cbmc/stubs/snprintf.c
new file mode 100644
index 00000000..bfb992e2
--- /dev/null
+++ b/test/cbmc/stubs/snprintf.c
@@ -0,0 +1,42 @@
+/*
+ * FreeRTOS-Cellular-Interface v1.1.0
+ * Copyright (C) 2021 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ */
+
+/**
+ * @file snprintf.c
+ * @brief Creates a stub for snprintf. This stub checks if, for the input copy
+ * length, the destination and source are valid accessible memory.
+ */
+
+#include <stdio.h>
+
+int snprintf( char * s,
+              size_t n,
+              const char * format,
+              ... )
+{
+    __CPROVER_assert( __CPROVER_w_ok( s, n ), "write" );
+    __CPROVER_assert( __CPROVER_r_ok( s, n ), "read" );
+    return n;
+}
diff --git a/test/cbmc/stubs/strchr.c b/test/cbmc/stubs/strchr.c
index 51568ed3..0ef77f4a 100644
--- a/test/cbmc/stubs/strchr.c
+++ b/test/cbmc/stubs/strchr.c
@@ -40,7 +40,7 @@
     char * __builtin___strchr_chk( const char * s,
                                    int c )
     {
-        if( ( __CPROVER_w_ok( s, 1 ), "write" ) && ( __CPROVER_r_ok( s, 1 ), "read" ) )
+        if( __CPROVER_w_ok( s, 1 ) && __CPROVER_r_ok( s, 1 ) )
         {
             while( *s != '\0' )
             {
@@ -49,7 +49,7 @@
                     return s;
                 }
 
-                if( ( __CPROVER_w_ok( s + 1, 1 ), "write" ) && ( __CPROVER_r_ok( s + 1, 1 ), "read" ) )
+                if( __CPROVER_w_ok( s + 1, 1 ) && __CPROVER_r_ok( s + 1, 1 ) )
                 {
                     s++;
                 }
@@ -62,7 +62,7 @@
     char * strchr( const char * s,
                    int c )
     {
-        if( ( __CPROVER_w_ok( s, 1 ), "write" ) && ( __CPROVER_r_ok( s, 1 ), "read" ) )
+        if( __CPROVER_w_ok( s, 1 ) && __CPROVER_r_ok( s, 1 ) )
         {
             while( *s != '\0' )
             {
@@ -71,7 +71,7 @@
                     return s;
                 }
 
-                if( ( __CPROVER_w_ok( s + 1, 1 ), "write" ) && ( __CPROVER_r_ok( s + 1, 1 ), "read" ) )
+                if( __CPROVER_w_ok( s + 1, 1 ) && __CPROVER_r_ok( s + 1, 1 ) )
                 {
                     s++;
                 }
diff --git a/test/cbmc/stubs/strnlen.c b/test/cbmc/stubs/strnlen.c
new file mode 100644
index 00000000..fa6436aa
--- /dev/null
+++ b/test/cbmc/stubs/strnlen.c
@@ -0,0 +1,50 @@
+/*
+ * FreeRTOS-Cellular-Interface v1.1.0
+ * Copyright (C) 2021 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ */
+
+/**
+ * @file strnlen.c
+ * @brief Creates a stub for strnlen. This stub checks if, for the input copy
+ * length, the destination and source are valid accessible memory.
+ */
+
+#include <string.h>
+
+size_t strnlen( const char * s,
+                size_t n )
+{
+    size_t ret = 0;
+    char * pS = s;
+
+    while( *pS && ret < n )
+    {
+        pS++;
+        ret++;
+
+        __CPROVER_assert( __CPROVER_w_ok( pS, 1 ), "write" );
+        __CPROVER_assert( __CPROVER_r_ok( pS, 1 ), "read" );
+    }
+
+    return ret;
+}
diff --git a/test/cbmc/stubs/strstr.c b/test/cbmc/stubs/strstr.c
new file mode 100644
index 00000000..01303d0d
--- /dev/null
+++ b/test/cbmc/stubs/strstr.c
@@ -0,0 +1,51 @@
+/*
+ * FreeRTOS-Cellular-Interface v1.1.0
+ * Copyright (C) 2021 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * https://www.FreeRTOS.org
+ * https://github.com/FreeRTOS
+ */
+
+/**
+ * @file strstr.c
+ * @brief Creates a stub for strstr. This stub checks if, for the input copy
+ * length, the destination and source are valid accessible memory.
+ */
+
+#include <string.h>
+
+char * strstr( const char * s1,
+               const char * s2 )
+{
+    size_t offset = nondet_size_t();
+
+    __CPROVER_assert( __CPROVER_w_ok( s1, strlen( s1 ) ), "s1 write" );
+    __CPROVER_assert( __CPROVER_r_ok( s1, strlen( s1 ) ), "s1 read" );
+
+    __CPROVER_assert( __CPROVER_w_ok( s2, strlen( s2 ) ), "s2 write" );
+    __CPROVER_assert( __CPROVER_r_ok( s2, strlen( s2 ) ), "s2 read" );
+
+    if( ( offset >= 0 ) && ( offset < strlen( s1 ) ) )
+    {
+        return s1 + offset;
+    }
+
+    return NULL;
+}
diff --git a/test/cbmc/stubs/strtok.c b/test/cbmc/stubs/strtok.c
index 53bfcf89..b81350fe 100644
--- a/test/cbmc/stubs/strtok.c
+++ b/test/cbmc/stubs/strtok.c
@@ -29,6 +29,7 @@
  * length, the destination and source are valid accessible memory.
  */
 
+#include <stdio.h>
 #include <string.h>
 
 /* This is a clang macro not available on linux */
@@ -40,7 +41,7 @@
     char * __builtin___strtok( char * s,
                                const char * delim )
     {
-        if( ( __CPROVER_w_ok( s, 1 ), "write" ) && ( __CPROVER_r_ok( s, 1 ), "read" ) )
+        if( __CPROVER_w_ok( s, 1 ) && __CPROVER_r_ok( s, 1 ) )
         {
             while( *s != '\0' )
             {
@@ -49,7 +50,7 @@
                     return s;
                 }
 
-                if( ( __CPROVER_w_ok( s + 1, 1 ), "write" ) && ( __CPROVER_r_ok( s + 1, 1 ), "read" ) )
+                if( __CPROVER_w_ok( s + 1, 1 ) && __CPROVER_r_ok( s + 1, 1 ) )
                 {
                     s++;
                 }
@@ -67,3 +68,24 @@
         return s;
     }
 #endif /* if __has_builtin( __builtin___strchr ) */
+
+char * strtok_r( char * restrict s,
+                 const char * restrict sep,
+                 char ** restrict lasts )
+{
+    size_t offset = nondet_size_t();
+
+    ( void ) s;
+    ( void ) sep;
+    ( void ) lasts;
+
+    __CPROVER_assert( __CPROVER_w_ok( s, strlen( s ) ), "write" );
+    __CPROVER_assert( __CPROVER_r_ok( s, strlen( s ) ), "read" );
+
+    if( ( offset >= 0 ) && ( offset < strlen( s ) ) )
+    {
+        return s + offset;
+    }
+
+    return NULL;
+}