From 1042ea8cf8423e041237de9b8b79aab6d4bb9577 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Tue, 25 Oct 2022 13:22:10 -0400
Subject: [PATCH] Refined task control block predicate `TCB_p` such that it can
 be used to justify `memset`-ing the stack.

---
 tasks.c                                              |  4 ++--
 verification/verifast/preprocessed_files/tasks--pp.c | 10 +++++++---
 verification/verifast/proof/task_predicates.h        |  8 ++++++--
 3 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/tasks.c b/tasks.c
index 743b3c7f8..4d10e41b8 100644
--- a/tasks.c
+++ b/tasks.c
@@ -1356,12 +1356,12 @@ static void prvYieldForTask( TCB_t * pxTCB,
                     pxNewTCB = ( TCB_t * ) pvPortMalloc( sizeof( TCB_t ) ); /*lint !e9087 !e9079 All values returned by pvPortMalloc() have at least the alignment required by the MCU's stack, and the first member of TCB_t is always a pointer to the task's stack. */
 
                     if( pxNewTCB != NULL )
-                    {
+                    {   
                         /* Store the stack location in the TCB. */
                         pxNewTCB->pxStack = pxStack;
                         //@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _);
                         //@ close xLIST_ITEM(&pxNewTCB->xEventListItem, _, _, _, _);
-                        //@ close TCB_p(pxNewTCB); 
+                        //@ close TCB_p(pxNewTCB, ((size_t) usStackDepth) * sizeof(StackType_t)); 
                     }
                     else
                     {
diff --git a/verification/verifast/preprocessed_files/tasks--pp.c b/verification/verifast/preprocessed_files/tasks--pp.c
index 7acbdb895..8862550c4 100644
--- a/verification/verifast/preprocessed_files/tasks--pp.c
+++ b/verification/verifast/preprocessed_files/tasks--pp.c
@@ -81,7 +81,7 @@ predicate xLIST_ITEM(
 /*@
 // This predicate represents the memory corresponding to an
 // instance of type `TCB_t` aka `tskTaskControlBlock`.
-predicate TCB_p(TCB_t * tcb) =
+predicate TCB_p(TCB_t * tcb, int stackSize) =
     malloc_block_tskTaskControlBlock(tcb) &*&
     tcb->pxTopOfStack |-> _ &*&
 
@@ -91,7 +91,11 @@ predicate TCB_p(TCB_t * tcb) =
     struct_xLIST_ITEM_padding(&tcb->xEventListItem) &*&
     
     tcb->uxPriority |-> _ &*&
-    tcb->pxStack |-> _ &*&
+
+    tcb->pxStack |-> ?stackPtr &*&
+    chars_((char*) stackPtr, stackSize, _) &*&
+    malloc_block_chars((char*) stackPtr, stackSize) &*&
+
     tcb->xTaskRunState |-> _ &*&
     tcb->xIsIdle |-> _ &*&
     
@@ -10723,7 +10727,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
                         pxNewTCB->pxStack = pxStack;
                         //@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _);
                         //@ close xLIST_ITEM(&pxNewTCB->xEventListItem, _, _, _, _);
-                        //@ close TCB_p(pxNewTCB); 
+                        //@ close TCB_p(pxNewTCB, ((size_t) usStackDepth) * sizeof(StackType_t)); 
                     }
                     else
                     {
diff --git a/verification/verifast/proof/task_predicates.h b/verification/verifast/proof/task_predicates.h
index 308866bbe..71767c686 100644
--- a/verification/verifast/proof/task_predicates.h
+++ b/verification/verifast/proof/task_predicates.h
@@ -8,7 +8,7 @@
 /*@
 // This predicate represents the memory corresponding to an
 // instance of type `TCB_t` aka `tskTaskControlBlock`.
-predicate TCB_p(TCB_t * tcb) =
+predicate TCB_p(TCB_t * tcb, int stackSize) =
     malloc_block_tskTaskControlBlock(tcb) &*&
     tcb->pxTopOfStack |-> _ &*&
 
@@ -18,7 +18,11 @@ predicate TCB_p(TCB_t * tcb) =
     struct_xLIST_ITEM_padding(&tcb->xEventListItem) &*&
     
     tcb->uxPriority |-> _ &*&
-    tcb->pxStack |-> _ &*&
+
+    tcb->pxStack |-> ?stackPtr &*&
+    chars_((char*) stackPtr, stackSize, _) &*&
+    malloc_block_chars((char*) stackPtr, stackSize) &*&
+
     tcb->xTaskRunState |-> _ &*&
     tcb->xIsIdle |-> _ &*&