From 63d8c5afa8b47fc1acb9b43ff67a4b26d44ac44f Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Thu, 10 Nov 2022 12:51:20 -0500
Subject: [PATCH] Rewrote side-effectful assertion such that VeriFast can
 process it.

---
 tasks.c | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/tasks.c b/tasks.c
index cafebf385..4cb1c9f3f 100644
--- a/tasks.c
+++ b/tasks.c
@@ -4173,7 +4173,15 @@ void vTaskSwitchContext( BaseType_t xCoreID )
     {
         /* vTaskSwitchContext() must never be called from within a critical section.
          * This is not necessarily true for vanilla FreeRTOS, but it is for this SMP port. */
-        configASSERT( pxCurrentTCB->uxCriticalNesting == 0 );
+        #ifdef VERIFAST
+            /* Reason for rewrite: VeriFast cannot handle non-pure assertions. */
+            {
+                UBaseType_t nesting = pxCurrentTCB->uxCriticalNesting;
+                configASSERT( nesting == 0 );
+            }
+        #else
+            configASSERT( pxCurrentTCB->uxCriticalNesting == 0 );
+        #endif /* VERIFAST */
 
         if( uxSchedulerSuspended != ( UBaseType_t ) pdFALSE )
         {