From c679fe77d6441cd412dd253d953ee833dd25d740 Mon Sep 17 00:00:00 2001
From: Michael McInerney <michael.mcinerney@proofcraft.systems>
Date: Fri, 19 Jul 2024 17:08:16 +0930
Subject: [PATCH] mcs: use local variable in postpone

This eases verification by using a local variable
which remains unchanged during execution of the
function.

This preserves semantics since tcbSchedDequeue
will not modify the scTcb field of the given sc.

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
---
 src/kernel/thread.c | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/kernel/thread.c b/src/kernel/thread.c
index 4983a40d6c6..220545e6422 100644
--- a/src/kernel/thread.c
+++ b/src/kernel/thread.c
@@ -567,8 +567,11 @@ void scheduleTCB(tcb_t *tptr)
 #ifdef CONFIG_KERNEL_MCS
 void postpone(sched_context_t *sc)
 {
-    tcbSchedDequeue(sc->scTcb);
-    tcbReleaseEnqueue(sc->scTcb);
+    tcb_t *tcb = sc->scTcb;
+    assert(tcb != NULL);
+
+    tcbSchedDequeue(tcb);
+    tcbReleaseEnqueue(tcb);
     NODE_STATE_ON_CORE(ksReprogram, sc->scCore) = true;
 }