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

@@ -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;
 }