fix cbmc test

aws · Jun 17, 2022 · 7d743cf · 7d743cf
1 parent 49b40ea
commit 7d743cf
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/test/cbmc/proofs/OTA_Resume/Makefile b/test/cbmc/proofs/OTA_Resume/Makefile
@@ -21,6 +21,7 @@ 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
+RESTRICT_FUNCTION_POINTER += platformInSelftest.function_pointer_call.1/getPlatformImageStateStub
 
 # 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

diff --git a/test/cbmc/proofs/OTA_Resume/OTA_Resume_harness.c b/test/cbmc/proofs/OTA_Resume/OTA_Resume_harness.c
@@ -41,7 +41,8 @@ void OTA_Resume_harness()
 {
     OtaInterfaces_t otaInterface;
 
-    /* Initialize os timers. */
+    /* Initialize os timers and self-test state fetcher */
+    otaInterface.pal.getPlatformImageState = getPlatformImageStateStub;
     otaInterface.os.timer.start = startTimerStub;
     otaAgent.pOtaInterface = &otaInterface;