From dbf03a0ab2955a7eec9aa319938ca5e71d860bb0 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Wed, 16 Nov 2022 10:55:25 -0500
Subject: [PATCH] Introduced predicates to differentiate between public and
 private parts of a TCB.

---
 verification/verifast/proof/task_predicates.h | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/verification/verifast/proof/task_predicates.h b/verification/verifast/proof/task_predicates.h
index e2e7f9152..cf02d2d5b 100644
--- a/verification/verifast/proof/task_predicates.h
+++ b/verification/verifast/proof/task_predicates.h
@@ -93,4 +93,19 @@ predicate absTCB_p(TCB_t* tcb) =
     TCB_p(tcb, _);
 @*/
 
+/*@ 
+// We have to segment TCBs into:
+// (i) public parts that can be accessed by anyone after
+//     following the appropriote synchronization steps and
+// (ii) private parts that may only be used by the task itself
+//      which the TCB represents
+//
+// The predicates below will be expanded iteratively.
+
+predicate prvTCB_p(TCB_t* tcb, uint32_t ulFreeBytesOnStack);
+
+predicate pubTCB_p(TCB_t* tcb) =
+    tcb->uxCriticalNesting |-> ?uxCriticalNesting;
+@*/
+
 #endif /* TASKS_GH */
\ No newline at end of file