From b330847935742f70c761c71c008c52779ef94772 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Wed, 16 Nov 2022 14:26:37 -0500
Subject: [PATCH] Added preliminary post condition for `vTaskSwitchContext`

---
 tasks.c | 28 ++++++++++++++++++++--------
 1 file changed, 20 insertions(+), 8 deletions(-)

diff --git a/tasks.c b/tasks.c
index abf0b1670..cc7ab6f4d 100644
--- a/tasks.c
+++ b/tasks.c
@@ -4128,19 +4128,30 @@ BaseType_t xTaskIncrementTick( void )
 
 void vTaskSwitchContext( BaseType_t xCoreID )
 /*@ requires 0 <= xCoreID &*& xCoreID < configNUM_CORES &*&
-             locked(nil) &*&
-             [?f_ISR]isrLock() &*&
-             [?f_task]taskLock() &*& 
-             interruptState_p(xCoreID, ?state) &*&
-             xCoreID == coreID_f() &*&
-             interruptsDisabled_f(state) == true &*&
-             // opened predicate `coreLocalInterruptInv_p()`
+            xCoreID == coreID_f() &*&
+            // access to locks and disabled interrupts
+                locked(nil) &*&
+                [?f_ISR]isrLock() &*&
+                [?f_task]taskLock() &*& 
+                interruptState_p(xCoreID, ?state) &*&
+                interruptsDisabled_f(state) == true &*&
+            // opened predicate `coreLocalInterruptInv_p()`
                 pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& 
                 pubTCB_p(gCurrentTCB, 0) &*&
                 integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _);
 
 @*/
-//@ ensures true;
+/*@ ensures // all locks release and interrupts remain disabled
+                locked(nil) &*&
+                [f_ISR]isrLock() &*&
+                [f_task]taskLock() &*& 
+                interruptState_p(xCoreID, state) &*&
+            // opened predicate `coreLocalInterruptInv_p()`
+                pointer(&pxCurrentTCBs[coreID_f], ?gNewCurrentTCB) &*& 
+                pubTCB_p(gNewCurrentTCB, 0) &*&
+                integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _);
+            // Remark: the part of the post condition relating to TCBs will have to change.
+@*/
 {
     /* Acquire both locks:
      * - The ISR lock protects the ready list from simultaneous access by
@@ -4253,6 +4264,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
             #endif /* ( configUSE_NEWLIB_REENTRANT == 1 ) && ( configNEWLIB_REENTRANT_IS_DYNAMIC == 0 ) */
         }
     }
+    //@ close pubTCB_p(gCurrentTCB, 0);
     //@ close taskISRLockInv();
     //@ consume_taskISRLockInv();
     portRELEASE_ISR_LOCK();