From 99d46f9e515bb31cc711bd5d685c7a878c17a824 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Thu, 8 Dec 2022 08:45:17 -0500
Subject: [PATCH] Guarded unsafe decrements of `uxTopReadyPriority` and
 `uxCurrentPriority`

---
 tasks.c | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/tasks.c b/tasks.c
index 790603967..9c048fcc4 100644
--- a/tasks.c
+++ b/tasks.c
@@ -1365,7 +1365,15 @@ static void prvYieldForTask( TCB_t * pxTCB,
             {
                 if( xDecrementTopPriority != pdFALSE )
                 {
+#if VERIFAST
+    /* Reason for rewrite: Code not memory safe.
+     */
+                    if(uxTopReadyPriority > 0) {
+                        uxTopReadyPriority--;    
+                    }
+#else
                     uxTopReadyPriority--;
+#endif /* VERIFAST */
                     #if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) )
                         {
                             xPriorityDropped = pdTRUE;
@@ -1403,9 +1411,16 @@ static void prvYieldForTask( TCB_t * pxTCB,
             configASSERT( ( uxCurrentPriority > tskIDLE_PRIORITY ) || ( xTaskScheduled == pdTRUE ) );
 #endif /* VERIFAST */
 
-//@ assume(uxCurrentPriority > 0);
 
+#if VERIFAST
+    /* Reason for rewrite: Code not memory safe.
+     */
+            if(uxCurrentPriority > 0) {
+                uxCurrentPriority--;
+            }
+#else
             uxCurrentPriority--;
+#endif /* VERIFAST */
 
             // @ close xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners);
             // @ assert( xLIST(gReadyList, ?gReadyListSize, _, _, gCells, gVals, gOwners) );