From 54523ecdcec6497ccdf1959d3209f867c9ad5983 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Wed, 16 Nov 2022 13:53:22 -0500
Subject: [PATCH] Included global variables `pxCurrentTCBs` and
 `pxYieldingPendings` in interrupt invariant.

---
 tasks.c                                                | 4 +++-
 verification/verifast/proof/verifast_lock_predicates.h | 5 ++++-
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/tasks.c b/tasks.c
index 8ee8ae71a..4f0f498c2 100644
--- a/tasks.c
+++ b/tasks.c
@@ -4136,7 +4136,8 @@ void vTaskSwitchContext( BaseType_t xCoreID )
              interruptsDisabled_f(state) == true &*&
              // opened predicate `coreLocalInterruptInv_p()`
                 pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& 
-                pubTCB_p(gCurrentTCB, 0);
+                pubTCB_p(gCurrentTCB, 0) &*&
+                integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _);
 
 @*/
 //@ ensures true;
@@ -4176,6 +4177,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
             configASSERT( pxCurrentTCB->uxCriticalNesting == 0 );
         #endif /* VERIFAST */
 
+        //@ open taskISRLockInv();
         if( uxSchedulerSuspended != ( UBaseType_t ) pdFALSE )
         {
             /* The scheduler is currently suspended - do not allow a context
diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h
index f3b3fcbfb..4a0324bec 100644
--- a/verification/verifast/proof/verifast_lock_predicates.h
+++ b/verification/verifast/proof/verifast_lock_predicates.h
@@ -28,7 +28,10 @@ predicate interruptState_p(uint32_t coreID, uint32_t state);
 fixpoint bool interruptsDisabled_f(uint32_t);
 
 predicate coreLocalInterruptInv_p() =
-    pointer(&pxCurrentTCBs[coreID_f], _);
+    pointer(&pxCurrentTCBs[coreID_f], ?currentTCB) &*&
+    pubTCB_p(currentTCB, 0) &*&
+    integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _);
+
 
 predicate coreLocalLocked(uint32_t coreID);
 @*/