Update CBMC for Cellular_CommonInit

FreeRTOS · Jan 31, 2024 · 6d7d5b9 · 6d7d5b9
1 parent d12f5d2
commit 6d7d5b9
Show file tree

Hide file tree

Showing 3 changed files with 54 additions and 27 deletions.
diff --git 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
@@ -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
@@ -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 ) */
 
 /* ========================================================================== */