From df553bda2beebbbe21834c6a95274029aa365259 Mon Sep 17 00:00:00 2001
From: chinglee-iot <61685396+chinglee-iot@users.noreply.github.com>
Date: Wed, 31 Jan 2024 14:31:58 +0800
Subject: [PATCH] Update Cellular_CommonInit error handling (#163)
* Update Cellular_CommonInit error handling
* Update size table
* Update CBMC for Cellular_CommonInit
---
docs/doxygen/include/size_table.md | 4 +-
source/cellular_common_api.c | 61 ++++--
.../Cellular_CommonInit_harness.c | 4 +-
test/cbmc/proofs/Cellular_CommonInit/Makefile | 4 +-
test/cbmc/sources/cellular_modules.c | 73 +++---
test/unit-test/cellular_common_api_utest.c | 207 +++++++++++++++++-
6 files changed, 307 insertions(+), 46 deletions(-)
diff --git a/docs/doxygen/include/size_table.md b/docs/doxygen/include/size_table.md
index 1c39ee78..80795d8a 100644
--- a/docs/doxygen/include/size_table.md
+++ b/docs/doxygen/include/size_table.md
@@ -25,7 +25,7 @@
| cellular_common_api.c |
0.7K |
- 0.6K |
+ 0.7K |
| cellular_common.c |
@@ -45,6 +45,6 @@
| Total estimates |
15.1K |
- 13.6K |
+ 13.7K |
diff --git a/source/cellular_common_api.c b/source/cellular_common_api.c
index d6a7e167..e1189452 100644
--- a/source/cellular_common_api.c
+++ b/source/cellular_common_api.c
@@ -146,25 +146,58 @@ CellularError_t Cellular_CommonInit( CellularHandle_t * pCellularHandle,
CellularError_t cellularStatus = CELLULAR_SUCCESS;
CellularContext_t * pContext = NULL;
- /* Init the common library. */
- cellularStatus = _Cellular_LibInit( pCellularHandle, pCommInterface, pTokenTable );
-
- /* Init the module. */
- if( cellularStatus == CELLULAR_SUCCESS )
+ if( pCellularHandle == NULL )
{
- pContext = *pCellularHandle;
- cellularStatus = Cellular_ModuleInit( pContext, &pContext->pModuleContext );
+ LogError( ( "Cellular_CommonInit pCellularHandle is NULL." ) );
+ cellularStatus = CELLULAR_INVALID_HANDLE;
}
-
- /* Setup UE, URC and query register status. */
- if( cellularStatus == CELLULAR_SUCCESS )
+ else if( pCommInterface == NULL )
{
- cellularStatus = Cellular_ModuleEnableUE( pContext );
+ LogError( ( "Cellular_CommonInit pCommInterface is NULL." ) );
+ cellularStatus = CELLULAR_BAD_PARAMETER;
}
-
- if( cellularStatus == CELLULAR_SUCCESS )
+ else if( pTokenTable == NULL )
+ {
+ LogError( ( "Cellular_CommonInit pTokenTable is NULL." ) );
+ cellularStatus = CELLULAR_BAD_PARAMETER;
+ }
+ else
{
- cellularStatus = Cellular_ModuleEnableUrc( pContext );
+ /* Init the common library. */
+ cellularStatus = _Cellular_LibInit( pCellularHandle, pCommInterface, pTokenTable );
+
+ if( cellularStatus == CELLULAR_SUCCESS )
+ {
+ pContext = ( CellularContext_t * ) ( *pCellularHandle );
+
+ cellularStatus = Cellular_ModuleInit( pContext, &pContext->pModuleContext );
+
+ if( cellularStatus == CELLULAR_SUCCESS )
+ {
+ cellularStatus = Cellular_ModuleEnableUE( pContext );
+
+ if( cellularStatus == CELLULAR_SUCCESS )
+ {
+ cellularStatus = Cellular_ModuleEnableUrc( pContext );
+ }
+
+ if( cellularStatus != CELLULAR_SUCCESS )
+ {
+ /* Clean up the resource allocated by cellular module here if
+ * Cellular_ModuleEnableUE or Cellular_ModuleEnableUrc returns
+ * error. */
+ ( void ) Cellular_ModuleCleanUp( pContext );
+ }
+ }
+
+ if( cellularStatus != CELLULAR_SUCCESS )
+ {
+ /* Clean up the resource in cellular common library if any of the
+ * module port function returns error. Error returned by _Cellular_LibInit
+ * is already handled in the implementation. */
+ ( void ) _Cellular_LibCleanup( pContext );
+ }
+ }
}
return cellularStatus;
diff --git a/test/cbmc/proofs/Cellular_CommonInit/Cellular_CommonInit_harness.c b/test/cbmc/proofs/Cellular_CommonInit/Cellular_CommonInit_harness.c
index 7ffc118d..5e1e9beb 100644
--- a/test/cbmc/proofs/Cellular_CommonInit/Cellular_CommonInit_harness.c
+++ b/test/cbmc/proofs/Cellular_CommonInit/Cellular_CommonInit_harness.c
@@ -96,5 +96,7 @@ void harness()
* Initialize the member of Cellular_CommonInit.
****************************************************************/
- Cellular_CommonInit( nondet_bool() ? NULL : &pHandle, &CellularCommInterface, &tokenTable );
+ Cellular_CommonInit( nondet_bool() ? NULL : &pHandle,
+ nondet_bool() ? NULL : &CellularCommInterface,
+ nondet_bool() ? NULL : &tokenTable );
}
diff --git a/test/cbmc/proofs/Cellular_CommonInit/Makefile b/test/cbmc/proofs/Cellular_CommonInit/Makefile
index 956dd779..dd991480 100755
--- a/test/cbmc/proofs/Cellular_CommonInit/Makefile
+++ b/test/cbmc/proofs/Cellular_CommonInit/Makefile
@@ -24,7 +24,7 @@ HARNESS_ENTRY=harness
HARNESS_FILE=Cellular_CommonInit_harness
PROOF_UID = Cellular_CommonInit
-DEFINES +=
+DEFINES += -DCBMC_TEST_CELLULAR_MODULE_RETURN_ERROR=1
INCLUDES +=
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
@@ -35,4 +35,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/cellular_modules.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common_api.c
PROJECT_SOURCES += $(SRCDIR)/source/cellular_common.c
+UNWINDSET += __CPROVER_file_local_cellular_common_c_libClose.0:20
+
include ../Makefile.common
diff --git a/test/cbmc/sources/cellular_modules.c b/test/cbmc/sources/cellular_modules.c
index 489e0847..471d2360 100644
--- a/test/cbmc/sources/cellular_modules.c
+++ b/test/cbmc/sources/cellular_modules.c
@@ -33,41 +33,64 @@
/* 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();
+#if ( CBMC_TEST_CELLULAR_MODULE_RETURN_ERROR == 1 )
- __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN );
- return ret;
-}
+ 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();
+ CellularError_t Cellular_ModuleCleanUp( const CellularContext_t * pContext )
+ {
+ CellularError_t ret = nondet_int();
- __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN );
- return ret;
-}
+ __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN );
+ return ret;
+ }
+ CellularError_t Cellular_ModuleEnableUE( CellularContext_t * pContext )
+ {
+ CellularError_t ret = nondet_int();
-CellularError_t Cellular_ModuleEnableUE( CellularContext_t * pContext )
-{
- CellularError_t ret = nondet_int();
+ __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN );
+ return ret;
+ }
- __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;
+ }
-CellularError_t Cellular_ModuleEnableUrc( CellularContext_t * pContext )
-{
- CellularError_t ret = nondet_int();
+#else /* #if ( CBMC_TEST_CELLULAR_MODULE_NO_ERROR == 1 ) */
- __CPROVER_assume( ret >= CELLULAR_SUCCESS && ret <= CELLULAR_UNKNOWN );
- return ret;
-}
+ CellularError_t Cellular_ModuleInit( const CellularContext_t * pContext,
+ void ** ppModuleContext )
+ {
+ return CELLULAR_SUCCESS;
+ }
+ CellularError_t Cellular_ModuleCleanUp( const CellularContext_t * pContext )
+ {
+ return CELLULAR_SUCCESS;
+ }
+
+ CellularError_t Cellular_ModuleEnableUE( CellularContext_t * pContext )
+ {
+ return CELLULAR_SUCCESS;
+ }
+
+ CellularError_t Cellular_ModuleEnableUrc( CellularContext_t * pContext )
+ {
+ return CELLULAR_SUCCESS;
+ }
+
+#endif /* #if ( CBMC_TEST_CELLULAR_MODULE_NO_ERROR == 1 ) */
/* ========================================================================== */
diff --git a/test/unit-test/cellular_common_api_utest.c b/test/unit-test/cellular_common_api_utest.c
index 787afa06..a0017f68 100644
--- a/test/unit-test/cellular_common_api_utest.c
+++ b/test/unit-test/cellular_common_api_utest.c
@@ -277,19 +277,220 @@ static CellularCommInterface_t cellularCommInterface =
/* ========================================================================== */
/**
- * @brief Test that null handler case for Cellular_CommonInit.
+ * @brief Cellular_CommonInit - Test the null pCommInterface parameter.
+ *
+ * Coverage
+ * @code{c}
+ * if( pCellularHandle == NULL )
+ * {
+ * LogError( ( "Cellular_CommonInit pCellularHandle is NULL." ) );
+ * cellularStatus = CELLULAR_INVALID_HANDLE;
+ * }
+ * @endcode
+ * ( pCellularHandle == NULL ) is true.
*/
void test_Cellular_CommonInit_Null_Handler( void )
{
CellularError_t cellularStatus = CELLULAR_SUCCESS;
- _Cellular_LibInit_IgnoreAndReturn( CELLULAR_INVALID_HANDLE );
-
+ /* API call. */
cellularStatus = Cellular_CommonInit( NULL, &cellularCommInterface, &tokenTable );
+ /* Verification. */
TEST_ASSERT_EQUAL( CELLULAR_INVALID_HANDLE, cellularStatus );
}
+/**
+ * @brief Cellular_CommonInit - Test the null pCommInterface parameter.
+ *
+ * Coverage
+ * @code{c}
+ * else if( pCommInterface == NULL )
+ * {
+ * LogError( ( "Cellular_CommonInit pCommInterface is NULL." ) );
+ * cellularStatus = CELLULAR_BAD_PARAMETER;
+ * }
+ * @endcode
+ * ( pCommInterface == NULL ) is true.
+ */
+void test_Cellular_CommonInit_Null_Comm_Interface( void )
+{
+ struct CellularContext * pHandler;
+ CellularError_t cellularStatus = CELLULAR_SUCCESS;
+
+ /* API call. */
+ cellularStatus = Cellular_CommonInit( &pHandler, NULL, &tokenTable );
+
+ /* Verification. */
+ TEST_ASSERT_EQUAL( CELLULAR_BAD_PARAMETER, cellularStatus );
+}
+
+/**
+ * @brief Cellular_CommonInit - Test the null pTokenTable parameter.
+ *
+ * Coverage
+ * @code{c}
+ * else if( pTokenTable == NULL )
+ * {
+ * LogError( ( "Cellular_CommonInit pTokenTable is NULL." ) );
+ * cellularStatus = CELLULAR_BAD_PARAMETER;
+ * }
+ * @endcode
+ * ( pTokenTable == NULL ) is true.
+ */
+void test_Cellular_CommonInit_Null_Token_Table( void )
+{
+ struct CellularContext * pHandler;
+ CellularError_t cellularStatus = CELLULAR_SUCCESS;
+
+ /* API call. */
+ cellularStatus = Cellular_CommonInit( &pHandler, &cellularCommInterface, NULL );
+
+ /* Verification. */
+ TEST_ASSERT_EQUAL( CELLULAR_BAD_PARAMETER, cellularStatus );
+}
+
+/**
+ * @brief Cellular_CommonInit - Test that _Cellular_LibInit returns error.
+ *
+ * Coverage
+ * @code{c}
+ * cellularStatus = _Cellular_LibInit( pCellularHandle, pCommInterface, pTokenTable );
+ * ...
+ * if( cellularStatus == CELLULAR_SUCCESS )
+ * {
+ * ...
+ * }
+ * @endcode
+ * ( cellularStatus == CELLULAR_SUCCESS ) is false.
+ */
+void test_Cellular_CommonInit_Lib_Init_error( void )
+{
+ struct CellularContext * pHandler;
+ CellularError_t cellularStatus = CELLULAR_SUCCESS;
+
+ /* Expectation. */
+ _Cellular_LibInit_IgnoreAndReturn( CELLULAR_RESOURCE_CREATION_FAIL );
+
+ /* API call. */
+ cellularStatus = Cellular_CommonInit( &pHandler, &cellularCommInterface, &tokenTable );
+
+ /* Verification. */
+ TEST_ASSERT_EQUAL( CELLULAR_RESOURCE_CREATION_FAIL, cellularStatus );
+}
+
+/**
+ * @brief Cellular_CommonInit - Test that Cellular_ModuleInit returns error.
+ *
+ * Coverage
+ * @code{c}
+ * cellularStatus = Cellular_ModuleInit( pContext, &pContext->pModuleContext );
+ * ...
+ * if( cellularStatus != CELLULAR_SUCCESS )
+ * {
+ * ( void ) _Cellular_LibCleanup( pContext );
+ * }
+ * @endcode
+ * ( cellularStatus != CELLULAR_SUCCESS ) is true.
+ */
+void test_Cellular_CommonInit_Module_Init_error( void )
+{
+ struct CellularContext xCellularContext = { 0 };
+ struct CellularContext * pContext;
+ CellularError_t cellularStatus = CELLULAR_SUCCESS;
+
+ /* Setup. */
+ pContext = &xCellularContext;
+
+ /* Expectation. */
+ _Cellular_LibInit_IgnoreAndReturn( CELLULAR_SUCCESS );
+ Cellular_ModuleInit_ExpectAndReturn( &xCellularContext, &xCellularContext.pModuleContext, CELLULAR_INTERNAL_FAILURE );
+ _Cellular_LibCleanup_ExpectAndReturn( &xCellularContext, CELLULAR_SUCCESS );
+
+ /* API call. */
+ cellularStatus = Cellular_CommonInit( &pContext, &cellularCommInterface, &tokenTable );
+
+ /* Verification. */
+ TEST_ASSERT_EQUAL( CELLULAR_INTERNAL_FAILURE, cellularStatus );
+}
+
+/**
+ * @brief Cellular_CommonInit - Test that Cellular_ModuleEnableUE returns error.
+ *
+ * Coverage
+ * @code{c}
+ * cellularStatus = Cellular_ModuleEnableUE( pContext );
+ * if( cellularStatus == CELLULAR_SUCCESS )
+ * {
+ * cellularStatus = Cellular_ModuleEnableUrc( pContext );
+ * }
+ * @endcode
+ * ( cellularStatus == CELLULAR_SUCCESS ) is false.
+ */
+void test_Cellular_CommonInit_Module_Enable_UE_error( void )
+{
+ struct CellularContext xCellularContext = { 0 };
+ struct CellularContext * pContext;
+ CellularError_t cellularStatus = CELLULAR_SUCCESS;
+
+ /* Setup. */
+ pContext = &xCellularContext;
+
+ /* Expectation. */
+ _Cellular_LibInit_IgnoreAndReturn( CELLULAR_SUCCESS );
+ Cellular_ModuleInit_ExpectAndReturn( &xCellularContext, &xCellularContext.pModuleContext, CELLULAR_SUCCESS );
+ Cellular_ModuleEnableUE_ExpectAndReturn( &xCellularContext, CELLULAR_INTERNAL_FAILURE );
+
+ Cellular_ModuleCleanUp_ExpectAndReturn( &xCellularContext, CELLULAR_SUCCESS );
+ _Cellular_LibCleanup_ExpectAndReturn( &xCellularContext, CELLULAR_SUCCESS );
+
+ /* API call. */
+ cellularStatus = Cellular_CommonInit( &pContext, &cellularCommInterface, &tokenTable );
+
+ /* Verification. */
+ TEST_ASSERT_EQUAL( CELLULAR_INTERNAL_FAILURE, cellularStatus );
+}
+
+/**
+ * @brief Cellular_CommonInit - Test that Cellular_ModuleEnableUrc returns error.
+ *
+ * Coverage
+ * @code{c}
+ * ...
+ * cellularStatus = Cellular_ModuleEnableUrc( pContext );
+ * ...
+ * if( cellularStatus != CELLULAR_SUCCESS )
+ * {
+ * cellularStatus = Cellular_ModuleCleanUp( pContext );
+ * }
+ * @endcode
+ * ( cellularStatus != CELLULAR_SUCCESS ) is true.
+ */
+void test_Cellular_CommonInit_Module_Enable_URC_error( void )
+{
+ struct CellularContext xCellularContext = { 0 };
+ struct CellularContext * pContext;
+ CellularError_t cellularStatus = CELLULAR_SUCCESS;
+
+ /* Setup. */
+ pContext = &xCellularContext;
+
+ /* Expectation. */
+ _Cellular_LibInit_IgnoreAndReturn( CELLULAR_SUCCESS );
+ Cellular_ModuleInit_ExpectAndReturn( &xCellularContext, &xCellularContext.pModuleContext, CELLULAR_SUCCESS );
+ Cellular_ModuleEnableUE_ExpectAndReturn( &xCellularContext, CELLULAR_SUCCESS );
+ Cellular_ModuleEnableUrc_ExpectAndReturn( &xCellularContext, CELLULAR_INTERNAL_FAILURE );
+
+ Cellular_ModuleCleanUp_ExpectAndReturn( &xCellularContext, CELLULAR_SUCCESS );
+ _Cellular_LibCleanup_ExpectAndReturn( &xCellularContext, CELLULAR_SUCCESS );
+
+ /* API call. */
+ cellularStatus = Cellular_CommonInit( &pContext, &cellularCommInterface, &tokenTable );
+
+ /* Verification. */
+ TEST_ASSERT_EQUAL( CELLULAR_INTERNAL_FAILURE, cellularStatus );
+}
+
/**
* @brief Test that happy path case for Cellular_CommonInit.
*/