From 383a0558729eecd5b793d4ed3b1b4e96904b5fd5 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Wed, 16 Nov 2022 15:30:40 -0500
Subject: [PATCH] `taskCHECK_FOR_STACK_OVERFLOW` assumes minimal stack size.
 Updated stack predicate accordingly.

---
 verification/verifast/proof/stack_predicates.h | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/verification/verifast/proof/stack_predicates.h b/verification/verifast/proof/stack_predicates.h
index 6c2134721..b8eb15600 100644
--- a/verification/verifast/proof/stack_predicates.h
+++ b/verification/verifast/proof/stack_predicates.h
@@ -24,7 +24,11 @@ predicate stack_p_2(StackType_t * pxStack,
     integers_(pxTopOfStack + 1, sizeof(StackType_t), false, ulUsedCells, _) &*&
     // Unaligned rest
     unalignedRestOfStack_p((char*) pxStack + ulFreeBytes + sizeof(StackType_t) * ulUsedCells, 
-                           ulUnalignedBytes);
+                           ulUnalignedBytes) &*&
+    // `taskCHECK_FOR_STACK_OVERFLOW` macro on RP2040 port expects minimal stack size
+    ulFreeBytes >= 0 &*&
+    ulUsedCells >= 0 &*&
+    ulFreeBytes + ulUsedCells * sizeof(StackType_t) >= 3 * sizeof(StackType_t);
 
 predicate unalignedRestOfStack_p(char* p, uint32_t ulUnalignedBytes) =
     chars(p, ulUnalignedBytes, _);