From 0e84d8906fb5626cedda4fb09d2d8d25bcbac29d Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Wed, 2 Nov 2022 14:16:29 -0400
Subject: [PATCH] Updated stack depth requirements in preconditions to match
 precondition of `pxPortInitialiseStack`

---
 tasks.c                                              | 4 ++--
 verification/verifast/preprocessed_files/tasks--pp.c | 5 +++--
 verification/verifast/proof/task_predicates.h        | 1 +
 3 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/tasks.c b/tasks.c
index ff0e1c062..30d1d5c59 100644
--- a/tasks.c
+++ b/tasks.c
@@ -1315,7 +1315,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
                             UBaseType_t uxPriority,
                             TaskHandle_t * const pxCreatedTask )
     /*@ requires usStackDepth * sizeof( StackType_t ) < UINTPTR_MAX &*&
-                 usStackDepth > 2 &*&
+                 usStackDepth > 18 &*&
                  // We assume that macro `configMAX_TASK_NAME_LEN` evaluates to 16.
                  chars(pcName, 16, _);
      @*/
@@ -1445,7 +1445,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
 /*@ requires uninit_TCB_p(pxNewTCB, ?stackSize) &*&
              stackSize == ulStackDepth * sizeof(StackType_t) &*&
              stackSize <= UINTPTR_MAX &*&
-             ulStackDepth > 2 &*&
+             ulStackDepth > 18 &*&
              // We assume that macro `configMAX_TASK_NAME_LEN` evaluates to 16.
              chars(pcName, 16, _);
  @*/
diff --git a/verification/verifast/preprocessed_files/tasks--pp.c b/verification/verifast/preprocessed_files/tasks--pp.c
index d7bd2b194..3f2ef9fe1 100644
--- a/verification/verifast/preprocessed_files/tasks--pp.c
+++ b/verification/verifast/preprocessed_files/tasks--pp.c
@@ -10084,6 +10084,7 @@ predicate uninit_TCB_p(TCB_t * tcb, int stackSize) =
     tcb->uxPriority |-> _ &*&
 
     tcb->pxStack |-> ?stackPtr &*&
+    stackPtr != 0 &*&
     (char*) stackPtr + stackSize <=  (char*) UINTPTR_MAX &*&
     chars_((char*) stackPtr, stackSize, _) &*&
     malloc_block_chars((char*) stackPtr, stackSize) &*&
@@ -11208,7 +11209,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
                             UBaseType_t uxPriority,
                             TaskHandle_t * const pxCreatedTask )
     /*@ requires usStackDepth * sizeof( StackType_t ) < UINTPTR_MAX &*&
-                 usStackDepth > 2 &*&
+                 usStackDepth > 18 &*&
                  // We assume that macro `configMAX_TASK_NAME_LEN` evaluates to 16.
                  chars(pcName, 16, _);
      @*/
@@ -11290,7 +11291,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
 /*@ requires uninit_TCB_p(pxNewTCB, ?stackSize) &*&
              stackSize == ulStackDepth * sizeof(StackType_t) &*&
              stackSize <= UINTPTR_MAX &*&
-             ulStackDepth > 2 &*&
+             ulStackDepth > 18 &*&
              // We assume that macro `configMAX_TASK_NAME_LEN` evaluates to 16.
              chars(pcName, 16, _);
  @*/
diff --git a/verification/verifast/proof/task_predicates.h b/verification/verifast/proof/task_predicates.h
index 270f72207..85b1d3f1b 100644
--- a/verification/verifast/proof/task_predicates.h
+++ b/verification/verifast/proof/task_predicates.h
@@ -20,6 +20,7 @@ predicate uninit_TCB_p(TCB_t * tcb, int stackSize) =
     tcb->uxPriority |-> _ &*&
 
     tcb->pxStack |-> ?stackPtr &*&
+    stackPtr != 0 &*&
     (char*) stackPtr + stackSize <=  (char*) UINTPTR_MAX &*&
     chars_((char*) stackPtr, stackSize, _) &*&
     malloc_block_chars((char*) stackPtr, stackSize) &*&