diff --git a/docs/doxygen/include/size_table.md b/docs/doxygen/include/size_table.md
index e49d7796e..8cd7919b7 100644
--- a/docs/doxygen/include/size_table.md
+++ b/docs/doxygen/include/size_table.md
@@ -9,8 +9,8 @@
ota.c |
- 8.0K |
- 7.2K |
+ 8.1K |
+ 7.3K |
ota_interface.c |
@@ -39,7 +39,7 @@
Total estimates |
- 12.1K |
- 11.0K |
+ 12.2K |
+ 11.1K |
diff --git a/source/ota.c b/source/ota.c
index cfb315999..d521c293d 100644
--- a/source/ota.c
+++ b/source/ota.c
@@ -3186,6 +3186,14 @@ OtaState_t OTA_Shutdown( uint32_t ticksToWait,
{
otaAgent.unsubscribeOnShutdown = unsubscribeFlag;
+ /* Stop and delete the request timer. */
+ ( void ) otaAgent.pOtaInterface->os.timer.stop( OtaRequestTimer );
+ ( void ) otaAgent.pOtaInterface->os.timer.delete( OtaRequestTimer );
+
+ /* Stop and delete the self-test timer. */
+ ( void ) otaAgent.pOtaInterface->os.timer.stop( OtaSelfTestTimer );
+ ( void ) otaAgent.pOtaInterface->os.timer.delete( OtaSelfTestTimer );
+
/*
* Send shutdown signal to OTA Agent task.
*/
@@ -3386,6 +3394,9 @@ OtaErr_t OTA_Suspend( void )
/* Stop the request timer. */
( void ) otaAgent.pOtaInterface->os.timer.stop( OtaRequestTimer );
+ /* Stop the self-test timer. */
+ ( void ) otaAgent.pOtaInterface->os.timer.stop( OtaSelfTestTimer );
+
/*
* Send event to OTA agent task.
*/
@@ -3416,6 +3427,19 @@ OtaErr_t OTA_Resume( void )
/* Check if OTA Agent is running. */
if( otaAgent.state != OtaAgentStateStopped )
{
+ /*
+ * Resume timers.
+ */
+ ( void ) otaAgent.pOtaInterface->os.timer.start( OtaSelfTestTimer,
+ "OtaSelfTestTimer",
+ otaconfigSELF_TEST_RESPONSE_WAIT_MS,
+ otaTimerCallback );
+
+ ( void ) otaAgent.pOtaInterface->os.timer.start( OtaRequestTimer,
+ "OtaRequestTimer",
+ otaconfigFILE_REQUEST_WAIT_MS,
+ otaTimerCallback );
+
/*
* Send event to OTA agent task.
*/
diff --git a/test/cbmc/include/stubs.h b/test/cbmc/include/stubs.h
index 3023ad1e4..06ee6fb9a 100644
--- a/test/cbmc/include/stubs.h
+++ b/test/cbmc/include/stubs.h
@@ -109,3 +109,6 @@ OtaPalStatus_t createFilePalStub( OtaFileContext_t * const pFileContext );
/* Stub to request a fileblock from the Data plane. */
OtaErr_t requestFileBlockStub( OtaAgentContext_t * pAgentCtx );
+
+/* Stub to delete timer. */
+OtaOsStatus_t deleteTimerStub( OtaTimerId_t otaTimerId );
diff --git a/test/cbmc/proofs/OTA_Resume/Makefile b/test/cbmc/proofs/OTA_Resume/Makefile
index afe66b50d..fe0c71185 100644
--- a/test/cbmc/proofs/OTA_Resume/Makefile
+++ b/test/cbmc/proofs/OTA_Resume/Makefile
@@ -8,14 +8,20 @@ PROOF_UID = OTA_Resume_harness
INCLUDES += -I$(SRCDIR)/source/dependency/coreJSON/source/include/
INCLUDES += -I$(SRCDIR)/source/
+INCLUDES += -I$(SRCDIR)/test/cbmc/include/
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROJECT_SOURCES += $(SRCDIR)/source/ota.c
+DEFINES += -Dstatic=""
+
NONDET_STATIC += "--nondet-static"
REMOVE_FUNCTION_BODY += OTA_SignalEvent
+RESTRICT_FUNCTION_POINTER += OTA_Resume.function_pointer_call.1/startTimerStub
+RESTRICT_FUNCTION_POINTER += OTA_Resume.function_pointer_call.2/startTimerStub
+
# If this proof is found to consume huge amounts of RAM, you can set the
# EXPENSIVE variable. With new enough versions of the proof tools, this will
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
diff --git a/test/cbmc/proofs/OTA_Resume/OTA_Resume_harness.c b/test/cbmc/proofs/OTA_Resume/OTA_Resume_harness.c
index 8f365f43f..bdeb87ec8 100644
--- a/test/cbmc/proofs/OTA_Resume/OTA_Resume_harness.c
+++ b/test/cbmc/proofs/OTA_Resume/OTA_Resume_harness.c
@@ -26,6 +26,9 @@
*/
/* Ota Agent includes. */
#include "ota.h"
+#include "stubs.h"
+
+extern OtaAgentContext_t otaAgent;
bool OTA_SignalEvent( const OtaEventMsg_t * const pEventMsg )
{
@@ -36,5 +39,11 @@ bool OTA_SignalEvent( const OtaEventMsg_t * const pEventMsg )
void OTA_Resume_harness()
{
+ OtaInterfaces_t otaInterface;
+
+ /* Initialize os timers. */
+ otaInterface.os.timer.start = startTimerStub;
+ otaAgent.pOtaInterface = &otaInterface;
+
OTA_Resume();
}
diff --git a/test/cbmc/proofs/OTA_Shutdown/Makefile b/test/cbmc/proofs/OTA_Shutdown/Makefile
index 8fca2a478..f71b7c48b 100644
--- a/test/cbmc/proofs/OTA_Shutdown/Makefile
+++ b/test/cbmc/proofs/OTA_Shutdown/Makefile
@@ -18,6 +18,11 @@ PROJECT_SOURCES += $(SRCDIR)/source/ota.c
REMOVE_FUNCTION_BODY += OTA_SignalEvent
+RESTRICT_FUNCTION_POINTER += OTA_Shutdown.function_pointer_call.1/stopTimerStub
+RESTRICT_FUNCTION_POINTER += OTA_Shutdown.function_pointer_call.2/deleteTimerStub
+RESTRICT_FUNCTION_POINTER += OTA_Shutdown.function_pointer_call.3/stopTimerStub
+RESTRICT_FUNCTION_POINTER += OTA_Shutdown.function_pointer_call.4/deleteTimerStub
+
# If this proof is found to consume huge amounts of RAM, you can set the
# EXPENSIVE variable. With new enough versions of the proof tools, this will
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
diff --git a/test/cbmc/proofs/OTA_Shutdown/OTA_Shutdown_harness.c b/test/cbmc/proofs/OTA_Shutdown/OTA_Shutdown_harness.c
index 73dfb3c46..2e6d75353 100644
--- a/test/cbmc/proofs/OTA_Shutdown/OTA_Shutdown_harness.c
+++ b/test/cbmc/proofs/OTA_Shutdown/OTA_Shutdown_harness.c
@@ -26,6 +26,7 @@
*/
/* Ota Agent includes. */
#include "ota.h"
+#include "stubs.h"
extern OtaAgentContext_t otaAgent;
@@ -34,9 +35,16 @@ void OTA_Shutdown_harness()
OtaState_t state;
uint32_t ticksToWait;
uint8_t unsubscribeFlag;
+ OtaInterfaces_t otaInterface;
otaAgent.state = state;
+ /* Initialize os timers functions. */
+ otaInterface.os.timer.stop = stopTimerStub;
+ otaInterface.os.timer.delete = deleteTimerStub;
+
+ otaAgent.pOtaInterface = &otaInterface;
+
/* This assumption is required to have an upper bound on the unwinding of while loop in
* OTA_Shutdown. This does not model the exact behavior of the code since the limitation of CBMC
* is that it checks concurrent code in sequential manner.*/
diff --git a/test/cbmc/source/stubs.c b/test/cbmc/source/stubs.c
index 14965f43f..a2a6fa6d6 100644
--- a/test/cbmc/source/stubs.c
+++ b/test/cbmc/source/stubs.c
@@ -304,3 +304,16 @@ OtaErr_t requestFileBlockStub( OtaAgentContext_t * pAgentCtx )
return err;
}
+
+OtaOsStatus_t deleteTimerStub( OtaTimerId_t otaTimerId )
+{
+ OtaOsStatus_t status;
+
+ /* status must have values only from the OtaOsStatus_t enum. */
+ __CPROVER_assume( ( status >= OtaOsSuccess ) && ( status <= OtaOsTimerDeleteFailed ) );
+
+ __CPROVER_assert( ( otaTimerId == OtaSelfTestTimer ) || ( otaTimerId == OtaRequestTimer ),
+ "Error: Expected otaTimerId to be either OtaSelfTestTimer or OtaRequestTimer." );
+
+ return status;
+}