From 7675b3bbe4c5f26210dcf1b24b77209751497b8f Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Wed, 16 Nov 2022 15:28:33 -0500
Subject: [PATCH] Rewrote macro `taskCHECK_FOR_STACK_OVERFLOW` such that VF can
 handle it.

---
 include/stack_macros.h | 48 ++++++++++++++++++++++++++++++------------
 1 file changed, 35 insertions(+), 13 deletions(-)

diff --git a/include/stack_macros.h b/include/stack_macros.h
index a80613712..55fa33ee3 100644
--- a/include/stack_macros.h
+++ b/include/stack_macros.h
@@ -84,19 +84,41 @@
 
 #if ( ( configCHECK_FOR_STACK_OVERFLOW > 1 ) && ( portSTACK_GROWTH < 0 ) )
 
-    #define taskCHECK_FOR_STACK_OVERFLOW()                                                            \
-    {                                                                                                 \
-        const uint32_t * const pulStack = ( uint32_t * ) pxCurrentTCB->pxStack;                       \
-        const uint32_t ulCheckValue = ( uint32_t ) 0xa5a5a5a5;                                        \
-                                                                                                      \
-        if( ( pulStack[ 0 ] != ulCheckValue ) ||                                                      \
-            ( pulStack[ 1 ] != ulCheckValue ) ||                                                      \
-            ( pulStack[ 2 ] != ulCheckValue ) ||                                                      \
-            ( pulStack[ 3 ] != ulCheckValue ) )                                                       \
-        {                                                                                             \
-            vApplicationStackOverflowHook( ( TaskHandle_t ) pxCurrentTCB, pxCurrentTCB->pcTaskName ); \
-        }                                                                                             \
-    }
+    #ifdef VERIFAST
+        /* Reason for rewrite: 
+         * VeriFast complains about unspecified evaluation order of
+         * `pxCurrentTCB->pxStack`.
+         *
+        */
+       #define taskCHECK_FOR_STACK_OVERFLOW()                                                            \
+        {                                                                                                \
+            TCB_t* tcb = pxCurrentTCB;                                                                   \
+            const uint32_t * const pulStack = ( uint32_t * ) tcb->pxStack;                      \
+            const uint32_t ulCheckValue = ( uint32_t ) 0xa5a5a5a5;                                        \
+                                                                                                        \
+            if( ( pulStack[ 0 ] != ulCheckValue ) ||                                                      \
+                ( pulStack[ 1 ] != ulCheckValue ) ||                                                      \
+                ( pulStack[ 2 ] != ulCheckValue ) ||                                                      \
+                ( pulStack[ 3 ] != ulCheckValue ) )                                                       \
+            {                                                                                             \
+                vApplicationStackOverflowHook( ( TaskHandle_t ) pxCurrentTCB, pxCurrentTCB->pcTaskName ); \
+            }                                                                                             \
+        }
+    #else
+        #define taskCHECK_FOR_STACK_OVERFLOW()                                                            \
+        {                                                                                                 \
+            const uint32_t * const pulStack = ( uint32_t * ) pxCurrentTCB->pxStack;                       \
+            const uint32_t ulCheckValue = ( uint32_t ) 0xa5a5a5a5;                                        \
+                                                                                                        \
+            if( ( pulStack[ 0 ] != ulCheckValue ) ||                                                      \
+                ( pulStack[ 1 ] != ulCheckValue ) ||                                                      \
+                ( pulStack[ 2 ] != ulCheckValue ) ||                                                      \
+                ( pulStack[ 3 ] != ulCheckValue ) )                                                       \
+            {                                                                                             \
+                vApplicationStackOverflowHook( ( TaskHandle_t ) pxCurrentTCB, pxCurrentTCB->pcTaskName ); \
+            }                                                                                             \
+        }
+    #endif /* VERIFAST */
 
 #endif /* #if( configCHECK_FOR_STACK_OVERFLOW > 1 ) */
 /*-----------------------------------------------------------*/