diff --git a/include/portable.h b/include/portable.h
index 246a8373b..d9bb2e720 100644
--- a/include/portable.h
+++ b/include/portable.h
@@ -128,8 +128,8 @@
         StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
                                              TaskFunction_t pxCode,
                                              void * pvParameters ) PRIVILEGED_FUNCTION;
-        //@ requires true;
-        //@ ensures true;
+        ///@ requires true;
+        ///@ ensures true;
     #endif
 #endif /* if ( portUSING_MPU_WRAPPERS == 1 ) */
 
diff --git a/tasks.c b/tasks.c
index 302c581c2..1792c97ed 100644
--- a/tasks.c
+++ b/tasks.c
@@ -1371,6 +1371,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
                         //@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _);
                         //@ close xLIST_ITEM(&pxNewTCB->xEventListItem, _, _, _, _);
                         //@ close TCB_p(pxNewTCB, ((size_t) usStackDepth) * sizeof(StackType_t)); 
+                        //@ assert(false);
                     }
                     else
                     {
diff --git a/verification/verifast/preprocessed_files/tasks--pp.c b/verification/verifast/preprocessed_files/tasks--pp.c
index 91d2257e1..339004bf6 100644
--- a/verification/verifast/preprocessed_files/tasks--pp.c
+++ b/verification/verifast/preprocessed_files/tasks--pp.c
@@ -4449,8 +4449,8 @@ bool spin_lock_is_claimed(uint lock_num);
         StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
                                              TaskFunction_t pxCode,
                                              void * pvParameters ) ;
-        //@ requires true;
-        //@ ensures true;
+        ///@ requires true;
+        ///@ ensures true;
 
 
 
@@ -10032,7 +10032,12 @@ predicate TCB_p(TCB_t * tcb, int stackSize) =
 
 /*@
 // Axiomatizes that: 0 <= ptr <= 2^32 - 1
-lemma void uint32_t_ptr_range(uint32_t* ptr);
+//lemma void uint32_t_ptr_range(uint32_t* ptr);
+//requires true;
+//ensures 0 <= (int) ptr &*& (int) ptr <= 4294967295;
+
+// Axiomatizes that: 0 <= ptr <= 2^32 - 1
+lemma void ptr_range<t>(t* ptr);
 requires true;
 ensures 0 <= (int) ptr &*& (int) ptr <= 4294967295;
 @*/
@@ -10153,6 +10158,112 @@ bool assert_fct(bool b)
 
 
 
+/*
+ * Setup the timer to generate the tick interrupts.  The implementation in this
+ * file is weak to allow application writers to change the timer used to
+ * generate the tick interrupt.
+ */
+void vPortSetupTimerInterrupt( void );
+
+/*
+ * Exception handlers.
+ */
+void xPortPendSVHandler( void ) ;
+void xPortSysTickHandler( void );
+void vPortSVCHandler( void );
+
+/*
+ * Start first task is a separate function so it can be tested in isolation.
+ */
+static void vPortStartFirstTask( void ) ;
+
+/*
+ * Used to catch tasks that attempt to return from their implementing function.
+ */
+static void prvTaskExitError( void );
+
+/*@
+// Represents a stack that grows down.
+predicate stack_p(StackType_t * pxStack, uint32_t ulStackDepth, StackType_t * pxTopOfStack, uint32_t freeCells) =
+	integers_(pxStack, sizeof(StackType_t), false, ulStackDepth, _) &*&
+    ulStackDepth > 0 &*&
+    freeCells >= 0 &*&
+    pxTopOfStack == pxStack + freeCells -1 &*&
+    0 <= freeCells &*& freeCells <= ulStackDepth;
+//	usedMem == pxStack - pxTopOfStack
+//	freeMem == ulStackDepth - usedMem
+	//freeCells * sizeof(StackType_t) == ulStackDepth * sizeof(StackType_t) - ((char*) pxStack - (char*) pxTopOfStack) &*&
+//	usedCells * sizeof(StackType_t) == ((char*) pxStack - (char*) pxTopOfStack);
+@*/
+
+/*/@
+lemma void split_stack(StackType_t * pxStack, int offset)
+requires stack_p(pxStack,?ulStackDepth, ?pxTopOfStack, ?freeMem, _) &*& 0 <= offset &*& 
+                offset * sizeof(StackType_t) < ulStackDepth;
+ensures integers_(pxStack, sizeof(StackType_t), true, offset * sizeof(StackType_t), _) &*&
+                integers_(pxStack + offset * sizeof(StackType_t), sizeof(StackType_t), true, ulStackDepth - offset * sizeof(StackType_t), _) ;
+{
+	open stack_p(_, _, _, _);
+	integers__split(pxStack, offset * sizeof(StackType_t) );
+}
+@*/
+
+/*@
+lemma void getTopOfStack(StackType_t* pxStack, StackType_t* pxTopOfStack)
+requires stack_p(pxStack,?ulStackDepth, pxTopOfStack, ?freeCells) &*&
+                 freeCells > 0;
+ensures // free cells minus top cell
+        integers_(pxStack, sizeof(StackType_t), false, freeCells-1, _)	&*&
+        // top stack cell
+		integer_(pxStack + freeCells-1, sizeof(StackType_t), false, _) &*&
+        // used stack cells
+		integers_(pxStack + freeCells, sizeof(StackType_t), false, 
+                  ulStackDepth - freeCells, _) &*&
+        // stack contraints necessary to close `stack_p` again
+        ulStackDepth > 0 &*&
+        freeCells >= 0 &*&
+        pxTopOfStack == pxStack + freeCells -1 &*&
+        0 <= freeCells &*& freeCells <= ulStackDepth;
+{
+    open stack_p(_, _, _, _);
+    integers__split(pxStack, freeCells-1);
+    open integers_(pxStack + (freeCells-1), _, _, _, _);
+}
+@*/
+
+
+// -------------------------------------------------
+// Validate stack predicate
+
+/* Simulates creation and initialisation of a stack that grows down as on RP2040.
+ */
+StackType_t* test_stack_pred(uint32_t depth)
+/*@ requires depth * sizeof(StackType_t) <= UINTPTR_MAX &*&
+             depth <= UINT_MAX &*&
+             depth > 0;
+ @*/
+/*@ ensures result == 0 ? true : stack_p(result, depth, ?top, depth) &*&
+            malloc_block_chars((char*) result, depth * sizeof(StackType_t));
+@*/
+{
+ StackType_t * stack;
+
+
+    /* Allocate space for the stack used by the task being created. */
+    stack = (StackType_t*) malloc( ( ( ( size_t ) depth ) * sizeof( StackType_t ) ) );
+    if(stack == 0) return 0;
+
+    memset(stack, 0, (unsigned int ) depth * sizeof(StackType_t));
+
+    StackType_t* top = stack + depth -1;
+
+    //@ chars_to_integers_(stack, sizeof(StackType_t), false, depth); 
+    //@ close stack_p(stack, depth, top, depth);
+    // integers_(stack0, 4, false, depth, _)
+    return stack;
+}
+// -------------------------------------------------
+
 
 /*
  * See header file for description.
@@ -10160,21 +10271,44 @@ bool assert_fct(bool b)
 StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
                                      TaskFunction_t pxCode,
                                      void * pvParameters )
-//@ requires true;
-//@ ensures true;
+/*@ requires pxTopOfStack > 0 &*&
+             stack_p(?pxStack, ?ulStackDepth, pxTopOfStack, ulStackDepth) &*&
+             ulStackDepth > 16;
+  @*/
+//@ ensures stack_p(pxStack, ulStackDepth, pxTopOfStack-16, ulStackDepth-16);
 {
+    //@ StackType_t* oldTop = pxTopOfStack;
+    //@ open stack_p(pxStack, ulStackDepth, pxTopOfStack, ulStackDepth);
+    ///@ close stack_p(pxStack, ulStackDepth, pxTopOfStack-1, ulStackDepth-1);
+    ///@ getTopOfStack(pxStack, pxTopOfStack-1);
+    //@ integers__split(pxStack, ulStackDepth-2);
+
     /* Simulate the stack frame as it would be created by a context switch
      * interrupt. */
     pxTopOfStack--; /* Offset added to account for the way the MCU uses the stack on entry/exit of interrupts. */
     *pxTopOfStack = ( 0x01000000 ); /* xPSR */
     pxTopOfStack--;
+    //@ close integers_(oldTop-1, sizeof(StackType_t), false, 2, _);
+    //@ integers__join(pxStack);
+    //@ ptr_range<void>(pxCode);
+    //@ integers__split(pxStack, ulStackDepth-3);
     *pxTopOfStack = ( StackType_t ) pxCode; /* PC */
+    //@ close integers_(oldTop-2, sizeof(StackType_t), false, 3, _);
     pxTopOfStack--;
+    //@ ptr_range<void>(prvTaskExitError);
+    //@ integers__join(pxStack);
+    //@ integers__split(pxStack, ulStackDepth-4);
     *pxTopOfStack = ( StackType_t ) prvTaskExitError; /* LR */
+    //@ close integers_(oldTop-3, sizeof(StackType_t), false, 4, _);
+    //@ integers__join(pxStack);
     pxTopOfStack -= 5; /* R12, R3, R2 and R1. */
+    //@ ptr_range<void>(pvParameters);
+    //@ integers__split(pxStack, ulStackDepth-9);
     *pxTopOfStack = ( StackType_t ) pvParameters; /* R0 */
+    //@ close integers_(oldTop-8, sizeof(StackType_t), false, 9, _);
+    //@ integers__join(pxStack);
     pxTopOfStack -= 8; /* R11..R4. */
-
+    //@ close stack_p(pxStack, ulStackDepth, pxTopOfStack, ulStackDepth-16);
     return pxTopOfStack;
 }
 // # 56 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c" 2
@@ -10887,6 +11021,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
                         //@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _);
                         //@ close xLIST_ITEM(&pxNewTCB->xEventListItem, _, _, _, _);
                         //@ close TCB_p(pxNewTCB, ((size_t) usStackDepth) * sizeof(StackType_t)); 
+                        //@ assert(false);
                     }
                     else
                     {
@@ -10904,9 +11039,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
 
         if( pxNewTCB != 0 )
         {
-// # 1399 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 1400 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
             prvInitialiseNewTask( pxTaskCode, pcName, ( uint32_t ) usStackDepth, pvParameters, uxPriority, pxCreatedTask, pxNewTCB, 0 );
-// # 1408 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 1409 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
             prvAddNewTaskToReadyList( pxNewTCB );
             xReturn = ( ( ( char ) 1 ) );
         }
@@ -10944,7 +11079,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
 {
     StackType_t * pxTopOfStack;
     UBaseType_t x;
-// # 1462 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 1463 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
     //@ open TCB_p(_,_);
 
     /* Avoid dependency on memset() if it is not required. */
@@ -10986,14 +11121,14 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
             //@ assume( 0 <= (( (uint32_t) pxTopOfStack) & ~(7)) );
 
             // TODO: How can we prove this?
-            // Assume that now overflow occurs.
+            // Assume that no overflow occurs.
             //@ assume(  (((uint32_t) pxTopOfStack) & ~7) <= UINTPTR_MAX);
             pxTopOfStack = ( StackType_t * ) ( ( ( uint32_t ) pxTopOfStack ) & ( ~( ( uint32_t ) ( 0x0007 ) ) ) ); /*lint !e923 !e9033 !e9078 MISRA exception.  Avoiding casts between pointers and integers is not practical.  Size differences accounted for using portPOINTER_SIZE_TYPE type.  Checked by assert(). */
 
             /* Check the alignment of the calculated top of stack is correct. */
-// # 1522 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 1523 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
         }
-// # 1536 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 1537 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
     //@ close TCB_p(pxNewTCB, stackSize); 
 
     /* Store the task name in the TCB. */
@@ -11083,7 +11218,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
         {
             pxNewTCB->uxCriticalNesting = ( UBaseType_t ) 0U;
         }
-// # 1644 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 1645 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
         {
             /* Avoid compiler warning about unreferenced parameter. */
             ( void ) xRegions;
@@ -11110,7 +11245,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
             //@ uchars__to_chars_(pxNewTCB->ucNotifyState);
             memset( ( void * ) &( pxNewTCB->ucNotifyState[ 0 ] ), 0x00, sizeof( pxNewTCB->ucNotifyState ) );
         }
-// # 1682 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 1683 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
         {
 
                 /* Reason for rewrite: Assignment not type safe. */
@@ -11119,17 +11254,17 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
 
 
         }
-// # 1705 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 1706 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
     /* Initialize the TCB stack to look as if the task was already running,
      * but had been interrupted by the scheduler.  The return address is set
      * to the start of the task function. Once the stack has been initialised
      * the top of stack variable is updated. */
-// # 1733 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 1734 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
         {
             /* If the port has capability to detect stack overflow,
              * pass the stack end address to the stack initialization
              * function as well. */
-// # 1750 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 1751 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
                 {
                     pxNewTCB->pxTopOfStack = pxPortInitialiseStack( pxTopOfStack, pxTaskCode, pvParameters );
                 }
@@ -11340,7 +11475,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
 
                 if( xTaskRunningOnCore == xCoreID )
                 {
-                    (__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1960, "uxSchedulerSuspended == 0") : (void)0);
+                    (__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1961, "uxSchedulerSuspended == 0") : (void)0);
                     vTaskYieldWithinAPI();
                 }
                 else
@@ -11363,12 +11498,12 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
         TickType_t xTimeToWake;
         BaseType_t xAlreadyYielded, xShouldDelay = ( ( char ) 0 );
 
-        (__builtin_expect(!(pxPreviousWakeTime), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1983, "pxPreviousWakeTime") : (void)0);
-        (__builtin_expect(!(( xTimeIncrement > 0U )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1984, "( xTimeIncrement > 0U )") : (void)0);
+        (__builtin_expect(!(pxPreviousWakeTime), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1984, "pxPreviousWakeTime") : (void)0);
+        (__builtin_expect(!(( xTimeIncrement > 0U )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1985, "( xTimeIncrement > 0U )") : (void)0);
 
         vTaskSuspendAll();
         {
-            (__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1988, "uxSchedulerSuspended == 1") : (void)0);
+            (__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 1989, "uxSchedulerSuspended == 1") : (void)0);
 
             /* Minor optimisation.  The tick count cannot change in this
              * block. */
@@ -11454,7 +11589,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
         {
             vTaskSuspendAll();
             {
-                (__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2074, "uxSchedulerSuspended == 1") : (void)0);
+                (__builtin_expect(!(uxSchedulerSuspended == 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2075, "uxSchedulerSuspended == 1") : (void)0);
                                  ;
 
                 /* A task that is removed from the event list while the
@@ -11508,7 +11643,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
 
         const TCB_t * const pxTCB = xTask;
 
-        (__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2128, "pxTCB") : (void)0);
+        (__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2129, "pxTCB") : (void)0);
 
         vTaskEnterCritical();
         {
@@ -11684,7 +11819,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
         BaseType_t xYieldForTask = ( ( char ) 0 );
         BaseType_t xCoreID;
 
-        (__builtin_expect(!(( uxNewPriority < 32 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2304, "( uxNewPriority < 32 )") : (void)0);
+        (__builtin_expect(!(( uxNewPriority < 32 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2305, "( uxNewPriority < 32 )") : (void)0);
 
         /* Ensure the new priority is valid. */
         if( uxNewPriority >= ( UBaseType_t ) 32 )
@@ -11838,13 +11973,13 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
 
 
 /*-----------------------------------------------------------*/
-// # 2492 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 2493 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*-----------------------------------------------------------*/
-// # 2515 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 2516 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*-----------------------------------------------------------*/
-// # 2533 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 2534 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*-----------------------------------------------------------*/
-// # 2561 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 2562 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*-----------------------------------------------------------*/
 
 
@@ -11921,7 +12056,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
                     if( xTaskRunningOnCore == 0 )
                     {
                         /* The current task has just been suspended. */
-                        (__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2637, "uxSchedulerSuspended == 0") : (void)0);
+                        (__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2638, "uxSchedulerSuspended == 0") : (void)0);
                         vTaskYieldWithinAPI();
                     }
                     else
@@ -11935,7 +12070,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
                 {
                     vTaskExitCritical();
 
-                    (__builtin_expect(!(pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2651, "pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]") : (void)0);
+                    (__builtin_expect(!(pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2652, "pxTCB == pxCurrentTCBs[ xTaskRunningOnCore ]") : (void)0);
 
                     /* The scheduler is not running, but the task that was pointed
                      * to by pxCurrentTCB has just been suspended and pxCurrentTCB
@@ -11982,7 +12117,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
         /* Accesses xPendingReadyList so must be called from a critical section. */
 
         /* It does not make sense to check if the calling task is suspended. */
-        (__builtin_expect(!(xTask), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2698, "xTask") : (void)0);
+        (__builtin_expect(!(xTask), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2699, "xTask") : (void)0);
 
         /* Is the task being resumed actually in the suspended list? */
         if( ( ( ( &( pxTCB->xStateListItem ) )->pxContainer == ( &xSuspendedTaskList ) ) ? ( ( ( char ) 1 ) ) : ( ( ( char ) 0 ) ) ) != ( ( char ) 0 ) )
@@ -12031,7 +12166,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
 
 
         /* It does not make sense to resume the calling task. */
-        (__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2747, "xTaskToResume") : (void)0);
+        (__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2748, "xTaskToResume") : (void)0);
 
         /* The parameter cannot be NULL as it is impossible to resume the
          * currently executing task. It is also impossible to resume a task
@@ -12090,7 +12225,7 @@ static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
 
         UBaseType_t uxSavedInterruptStatus;
 
-        (__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2806, "xTaskToResume") : (void)0);
+        (__builtin_expect(!(xTaskToResume), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 2807, "xTaskToResume") : (void)0);
 
         /* RTOS ports that support interrupt nesting have the concept of a
          * maximum  system call (or maximum API call) interrupt priority.
@@ -12211,7 +12346,7 @@ static BaseType_t prvCreateIdleTasks( void )
         {
                                     ;
         }
-// # 2974 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 2975 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
             {
                 if( xCoreID == 0 )
                 {
@@ -12223,7 +12358,7 @@ static BaseType_t prvCreateIdleTasks( void )
                                            ( ( UBaseType_t ) 0x00 ), /* In effect ( tskIDLE_PRIORITY | portPRIVILEGE_BIT ), but tskIDLE_PRIORITY is zero. */
                                            &xIdleTaskHandle[ xCoreID ] ); /*lint !e961 MISRA exception, justified as it is not a redundant explicit cast to all supported compilers. */
                 }
-// # 2997 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 2998 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
             }
 
     }
@@ -12260,7 +12395,7 @@ void vTaskStartScheduler( void )
          * so interrupts will automatically get re-enabled when the first task
          * starts to run. */
         assert_fct(false);
-// # 3047 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 3048 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
         xNextTaskUnblockTime = ( TickType_t ) 0xffffffffUL;
         xSchedulerRunning = ( ( char ) 1 );
         xTickCount = ( TickType_t ) 0;
@@ -12292,7 +12427,7 @@ void vTaskStartScheduler( void )
         /* This line will only be reached if the kernel could not be started,
          * because there was not enough FreeRTOS heap to create the idle task
          * or the timer task. */
-        (__builtin_expect(!(xReturn != ( -1 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3078, "xReturn != ( -1 )") : (void)0);
+        (__builtin_expect(!(xReturn != ( -1 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3079, "xReturn != ( -1 )") : (void)0);
     }
 
     /* Prevent compiler warnings if INCLUDE_xTaskGetIdleTaskHandle is set to 0,
@@ -12357,7 +12492,7 @@ void vTaskSuspendAll( void )
     }
 }
 /*----------------------------------------------------------*/
-// # 3205 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 3206 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*----------------------------------------------------------*/
 
 BaseType_t xTaskResumeAll( void )
@@ -12380,7 +12515,7 @@ BaseType_t xTaskResumeAll( void )
 
             /* If uxSchedulerSuspended is zero then this function does not match a
              * previous call to vTaskSuspendAll(). */
-            (__builtin_expect(!(uxSchedulerSuspended), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3227, "uxSchedulerSuspended") : (void)0);
+            (__builtin_expect(!(uxSchedulerSuspended), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3228, "uxSchedulerSuspended") : (void)0);
 
             --uxSchedulerSuspended;
             vPortRecursiveLock(1, spin_lock_instance(15), ( ( char ) 0 ));
@@ -12538,7 +12673,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char
     /* If null is passed in here then the name of the calling task is being
      * queried. */
     pxTCB = ( ( ( xTaskToQuery ) == 0 ) ? xTaskGetCurrentTaskHandle() : ( xTaskToQuery ) );
-    (__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3385, "pxTCB") : (void)0);
+    (__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3386, "pxTCB") : (void)0);
     return &( pxTCB->pcTaskName[ 0 ] );
 }
 /*-----------------------------------------------------------*/
@@ -12631,7 +12766,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char
         TCB_t * pxTCB;
 
         /* Task names will be truncated to configMAX_TASK_NAME_LEN - 1 bytes. */
-        (__builtin_expect(!(strlen( pcNameToQuery ) < 16), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3478, "strlen( pcNameToQuery ) < 16") : (void)0);
+        (__builtin_expect(!(strlen( pcNameToQuery ) < 16), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3479, "strlen( pcNameToQuery ) < 16") : (void)0);
 
         vTaskSuspendAll();
         {
@@ -12727,7 +12862,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char
                          * each task in the Suspended state. */
                         uxTask += prvListTasksWithinSingleList( &( pxTaskStatusArray[ uxTask ] ), &xSuspendedTaskList, eSuspended );
                     }
-// # 3588 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 3589 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
                     {
                         if( pulTotalRunTime != 0 )
                         {
@@ -12755,7 +12890,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char
     {
         /* If xTaskGetIdleTaskHandle() is called before the scheduler has been
          * started, then xIdleTaskHandle will be NULL. */
-        (__builtin_expect(!(( xIdleTaskHandle != 0 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3615, "( xIdleTaskHandle != 0 )") : (void)0);
+        (__builtin_expect(!(( xIdleTaskHandle != 0 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3616, "( xIdleTaskHandle != 0 )") : (void)0);
         return &( xIdleTaskHandle[ 0 ] );
     }
 
@@ -12766,7 +12901,7 @@ char * pcTaskGetName( TaskHandle_t xTaskToQuery ) /*lint !e971 Unqualified char
  * This is to ensure vTaskStepTick() is available when user defined low power mode
  * implementations require configUSE_TICKLESS_IDLE to be set to a value other than
  * 1. */
-// # 3639 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 3640 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*----------------------------------------------------------*/
 
 BaseType_t xTaskCatchUpTicks( TickType_t xTicksToCatchUp )
@@ -12775,7 +12910,7 @@ BaseType_t xTaskCatchUpTicks( TickType_t xTicksToCatchUp )
 
     /* Must not be called with the scheduler suspended as the implementation
      * relies on xPendedTicks being wound down to 0 in xTaskResumeAll(). */
-    (__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3647, "uxSchedulerSuspended == 0") : (void)0);
+    (__builtin_expect(!(uxSchedulerSuspended == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3648, "uxSchedulerSuspended == 0") : (void)0);
 
     /* Use xPendedTicks to mimic xTicksToCatchUp number of ticks occurring when
      * the scheduler is suspended so the ticks are executed in xTaskResumeAll(). */
@@ -12794,7 +12929,7 @@ BaseType_t xTaskCatchUpTicks( TickType_t xTicksToCatchUp )
         TCB_t * pxTCB = xTask;
         BaseType_t xReturn;
 
-        (__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3666, "pxTCB") : (void)0);
+        (__builtin_expect(!(pxTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3667, "pxTCB") : (void)0);
 
         vTaskSuspendAll();
         {
@@ -12893,7 +13028,7 @@ BaseType_t xTaskIncrementTick( void )
 
             if( xConstTickCount == ( TickType_t ) 0U ) /*lint !e774 'if' does not always evaluate to false as it is looking for an overflow. */
             {
-                { List_t * pxTemp; (__builtin_expect(!(( ( ( ( pxDelayedTaskList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( char ) 1 ) : ( ( char ) 0 ) ) )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3765, "( ( ( ( pxDelayedTaskList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( char ) 1 ) : ( ( char ) 0 ) ) )") : (void)0); pxTemp = pxDelayedTaskList; pxDelayedTaskList = pxOverflowDelayedTaskList; pxOverflowDelayedTaskList = pxTemp; xNumOfOverflows++; prvResetNextTaskUnblockTime(); };
+                { List_t * pxTemp; (__builtin_expect(!(( ( ( ( pxDelayedTaskList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( char ) 1 ) : ( ( char ) 0 ) ) )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 3766, "( ( ( ( pxDelayedTaskList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? ( ( char ) 1 ) : ( ( char ) 0 ) ) )") : (void)0); pxTemp = pxDelayedTaskList; pxDelayedTaskList = pxOverflowDelayedTaskList; pxOverflowDelayedTaskList = pxTemp; xNumOfOverflows++; prvResetNextTaskUnblockTime(); };
             }
             else
             {
@@ -13076,13 +13211,13 @@ BaseType_t xTaskIncrementTick( void )
     return xSwitchRequired;
 }
 /*-----------------------------------------------------------*/
-// # 3977 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 3978 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*-----------------------------------------------------------*/
-// # 4001 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 4002 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*-----------------------------------------------------------*/
-// # 4026 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 4027 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*-----------------------------------------------------------*/
-// # 4059 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 4060 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*-----------------------------------------------------------*/
 
 void vTaskSwitchContext( BaseType_t xCoreID )
@@ -13100,7 +13235,7 @@ 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. */
-        (__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4076, "xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0") : (void)0);
+        (__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4077, "xTaskGetCurrentTaskHandle()->uxCriticalNesting == 0") : (void)0);
 
         if( uxSchedulerSuspended != ( UBaseType_t ) ( ( char ) 0 ) )
         {
@@ -13112,7 +13247,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
         {
             xYieldPendings[ xCoreID ] = ( ( char ) 0 );
                                     ;
-// # 4117 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 4118 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
             /* Check for stack overflow, if configured. */
             { const uint32_t * const pulStack = ( uint32_t * ) xTaskGetCurrentTaskHandle()->pxStack; const uint32_t ulCheckValue = ( uint32_t ) 0xa5a5a5a5; if( ( pulStack[ 0 ] != ulCheckValue ) || ( pulStack[ 1 ] != ulCheckValue ) || ( pulStack[ 2 ] != ulCheckValue ) || ( pulStack[ 3 ] != ulCheckValue ) ) { vApplicationStackOverflowHook( ( TaskHandle_t ) xTaskGetCurrentTaskHandle(), xTaskGetCurrentTaskHandle()->pcTaskName ); } };
 
@@ -13129,7 +13264,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
                                    ;
 
             /* After the new task is switched in, update the global errno. */
-// # 4151 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 4152 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
         }
     }
     vPortRecursiveLock(0, spin_lock_instance(14), ( ( char ) 0 ));
@@ -13140,7 +13275,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
 void vTaskPlaceOnEventList( List_t * const pxEventList,
                             const TickType_t xTicksToWait )
 {
-    (__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4161, "pxEventList") : (void)0);
+    (__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4162, "pxEventList") : (void)0);
 
     /* THIS FUNCTION MUST BE CALLED WITH EITHER INTERRUPTS DISABLED OR THE
      * SCHEDULER SUSPENDED AND THE QUEUE BEING ACCESSED LOCKED. */
@@ -13159,11 +13294,11 @@ void vTaskPlaceOnUnorderedEventList( List_t * pxEventList,
                                      const TickType_t xItemValue,
                                      const TickType_t xTicksToWait )
 {
-    (__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4180, "pxEventList") : (void)0);
+    (__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4181, "pxEventList") : (void)0);
 
     /* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED.  It is used by
      * the event groups implementation. */
-    (__builtin_expect(!(uxSchedulerSuspended != 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4184, "uxSchedulerSuspended != 0") : (void)0);
+    (__builtin_expect(!(uxSchedulerSuspended != 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4185, "uxSchedulerSuspended != 0") : (void)0);
 
     /* Store the item value in the event list item.  It is safe to access the
      * event list item here as interrupts won't access the event list item of a
@@ -13187,7 +13322,7 @@ void vTaskPlaceOnUnorderedEventList( List_t * pxEventList,
                                           TickType_t xTicksToWait,
                                           const BaseType_t xWaitIndefinitely )
     {
-        (__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4208, "pxEventList") : (void)0);
+        (__builtin_expect(!(pxEventList), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4209, "pxEventList") : (void)0);
 
         /* This function should not be called by application code hence the
          * 'Restricted' in its name.  It is not part of the public API.  It is
@@ -13235,14 +13370,14 @@ BaseType_t xTaskRemoveFromEventList( const List_t * const pxEventList )
      * This function assumes that a check has already been made to ensure that
      * pxEventList is not empty. */
     pxUnblockedTCB = ( ( &( ( pxEventList )->xListEnd ) )->pxNext->pvOwner ); /*lint !e9079 void * is used as this macro is used with timers and co-routines too.  Alignment is known to be fine as the type of the pointer stored and retrieved is the same. */
-    (__builtin_expect(!(pxUnblockedTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4256, "pxUnblockedTCB") : (void)0);
+    (__builtin_expect(!(pxUnblockedTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4257, "pxUnblockedTCB") : (void)0);
     ( void ) uxListRemove( &( pxUnblockedTCB->xEventListItem ) );
 
     if( uxSchedulerSuspended == ( UBaseType_t ) ( ( char ) 0 ) )
     {
         ( void ) uxListRemove( &( pxUnblockedTCB->xStateListItem ) );
         ; { if( ( ( pxUnblockedTCB )->uxPriority ) > uxTopReadyPriority ) { uxTopReadyPriority = ( ( pxUnblockedTCB )->uxPriority ); } }; vListInsertEnd( &( pxReadyTasksLists[ ( pxUnblockedTCB )->uxPriority ] ), &( ( pxUnblockedTCB )->xStateListItem ) ); ;
-// # 4277 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 4278 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
     }
     else
     {
@@ -13272,7 +13407,7 @@ void vTaskRemoveFromUnorderedEventList( ListItem_t * pxEventListItem,
 
     /* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED.  It is used by
      * the event flags implementation. */
-    (__builtin_expect(!(uxSchedulerSuspended != ( ( char ) 0 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4306, "uxSchedulerSuspended != ( ( char ) 0 )") : (void)0);
+    (__builtin_expect(!(uxSchedulerSuspended != ( ( char ) 0 )), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4307, "uxSchedulerSuspended != ( ( char ) 0 )") : (void)0);
 
     /* Store the new item value in the event list. */
     ( ( pxEventListItem )->xItemValue = ( xItemValue | 0x80000000UL ) );
@@ -13280,9 +13415,9 @@ void vTaskRemoveFromUnorderedEventList( ListItem_t * pxEventListItem,
     /* Remove the event list form the event flag.  Interrupts do not access
      * event flags. */
     pxUnblockedTCB = ( ( pxEventListItem )->pvOwner ); /*lint !e9079 void * is used as this macro is used with timers and co-routines too.  Alignment is known to be fine as the type of the pointer stored and retrieved is the same. */
-    (__builtin_expect(!(pxUnblockedTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4314, "pxUnblockedTCB") : (void)0);
+    (__builtin_expect(!(pxUnblockedTCB), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4315, "pxUnblockedTCB") : (void)0);
     ( void ) uxListRemove( pxEventListItem );
-// # 4331 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 4332 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
     /* Remove the task from the delayed list and add it to the ready list.  The
      * scheduler is suspended so interrupts will not be accessing the ready
      * lists. */
@@ -13301,7 +13436,7 @@ void vTaskRemoveFromUnorderedEventList( ListItem_t * pxEventListItem,
 
 void vTaskSetTimeOutState( TimeOut_t * const pxTimeOut )
 {
-    (__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4349, "pxTimeOut") : (void)0);
+    (__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4350, "pxTimeOut") : (void)0);
     vTaskEnterCritical();
     {
         pxTimeOut->xOverflowCount = xNumOfOverflows;
@@ -13324,8 +13459,8 @@ BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut,
 {
     BaseType_t xReturn;
 
-    (__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4372, "pxTimeOut") : (void)0);
-    (__builtin_expect(!(pxTicksToWait), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4373, "pxTicksToWait") : (void)0);
+    (__builtin_expect(!(pxTimeOut), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4373, "pxTimeOut") : (void)0);
+    (__builtin_expect(!(pxTicksToWait), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4374, "pxTicksToWait") : (void)0);
 
     vTaskEnterCritical();
     {
@@ -13447,7 +13582,7 @@ void vTaskMissedYield( void )
  *
  * @todo additional conditional compiles to remove this function.
  */
-// # 4555 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 4556 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*
  * -----------------------------------------------------------
  * The Idle task.
@@ -13477,7 +13612,7 @@ static void prvIdleTask( void * pvParameters )
         /* See if any tasks have deleted themselves - if so then the idle task
          * is responsible for freeing the deleted task's TCB and stack. */
         prvCheckTasksWaitingTermination();
-// # 4596 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 4597 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
             {
                 /* When using preemption tasks of equal priority will be
                  * timesliced.  If a task that is sharing the idle priority is ready
@@ -13498,16 +13633,16 @@ static void prvIdleTask( void * pvParameters )
                                             ;
                 }
             }
-// # 4632 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 4633 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
         /* This conditional compilation should use inequality to 0, not equality
          * to 1.  This is to ensure portSUPPRESS_TICKS_AND_SLEEP() is called when
          * user defined low power mode  implementations require
          * configUSE_TICKLESS_IDLE to be set to a value other than 1. */
-// # 4697 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 4698 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
     }
 }
 /*-----------------------------------------------------------*/
-// # 4747 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 4748 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*-----------------------------------------------------------*/
 
 
@@ -13521,7 +13656,7 @@ static void prvIdleTask( void * pvParameters )
         if( xIndex < 5 )
         {
             pxTCB = ( ( ( xTaskToSet ) == 0 ) ? xTaskGetCurrentTaskHandle() : ( xTaskToSet ) );
-            (__builtin_expect(!(pxTCB != 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4760, "pxTCB != 0") : (void)0);
+            (__builtin_expect(!(pxTCB != 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 4761, "pxTCB != 0") : (void)0);
             pxTCB->pvThreadLocalStoragePointers[ xIndex ] = pvValue;
         }
     }
@@ -13552,7 +13687,7 @@ static void prvIdleTask( void * pvParameters )
 
 
 /*-----------------------------------------------------------*/
-// # 4807 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 4808 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*-----------------------------------------------------------*/
 
 static void prvInitialiseTaskLists( void )
@@ -13654,7 +13789,7 @@ static void prvCheckTasksWaitingTermination( void )
             {
                 pxTaskStatus->uxBasePriority = pxTCB->uxBasePriority;
             }
-// # 4919 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 4920 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
             {
                 pxTaskStatus->ulRunTimeCounter = 0;
             }
@@ -13785,7 +13920,7 @@ static void prvCheckTasksWaitingTermination( void )
 
 
 /*-----------------------------------------------------------*/
-// # 5088 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 5089 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*-----------------------------------------------------------*/
 
 
@@ -13842,7 +13977,7 @@ static void prvCheckTasksWaitingTermination( void )
                 free( (void*) pxTCB->pxStack);
                 free( (void*) pxTCB);
             }
-// # 5171 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 5172 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
     }
 
 
@@ -14047,8 +14182,8 @@ static void prvResetNextTaskUnblockTime( void )
              * If the mutex is held by a task then it cannot be given from an
              * interrupt, and if a mutex is given by the holding task then it must
              * be the running state task. */
-            (__builtin_expect(!(pxTCB == xTaskGetCurrentTaskHandle()), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5375, "pxTCB == xTaskGetCurrentTaskHandle()") : (void)0);
-            (__builtin_expect(!(pxTCB->uxMutexesHeld), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5376, "pxTCB->uxMutexesHeld") : (void)0);
+            (__builtin_expect(!(pxTCB == xTaskGetCurrentTaskHandle()), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5376, "pxTCB == xTaskGetCurrentTaskHandle()") : (void)0);
+            (__builtin_expect(!(pxTCB->uxMutexesHeld), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5377, "pxTCB->uxMutexesHeld") : (void)0);
             ( pxTCB->uxMutexesHeld )--;
 
             /* Has the holder of the mutex inherited the priority of another
@@ -14134,7 +14269,7 @@ static void prvResetNextTaskUnblockTime( void )
         {
             /* If pxMutexHolder is not NULL then the holder must hold at least
              * one mutex. */
-            (__builtin_expect(!(pxTCB->uxMutexesHeld), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5462, "pxTCB->uxMutexesHeld") : (void)0);
+            (__builtin_expect(!(pxTCB->uxMutexesHeld), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5463, "pxTCB->uxMutexesHeld") : (void)0);
 
             /* Determine the priority to which the priority of the task that
              * holds the mutex should be set.  This will be the greater of the
@@ -14161,7 +14296,7 @@ static void prvResetNextTaskUnblockTime( void )
                     /* If a task has timed out because it already holds the
                      * mutex it was trying to obtain then it cannot of inherited
                      * its own priority. */
-                    (__builtin_expect(!(pxTCB != xTaskGetCurrentTaskHandle()), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5489, "pxTCB != xTaskGetCurrentTaskHandle()") : (void)0);
+                    (__builtin_expect(!(pxTCB != xTaskGetCurrentTaskHandle()), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5490, "pxTCB != xTaskGetCurrentTaskHandle()") : (void)0);
 
                     /* Disinherit the priority, remembering the previous
                      * priority to facilitate determining the subject task's
@@ -14292,7 +14427,7 @@ void vTaskYieldWithinAPI( void )
         {
             /* If pxCurrentTCB->uxCriticalNesting is zero then this function
              * does not match a previous call to vTaskEnterCritical(). */
-            (__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5620, "xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U") : (void)0);
+            (__builtin_expect(!(xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5621, "xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U") : (void)0);
 
             if( xTaskGetCurrentTaskHandle()->uxCriticalNesting > 0U )
             {
@@ -14342,11 +14477,11 @@ void vTaskYieldWithinAPI( void )
 
 
 /*-----------------------------------------------------------*/
-// # 5696 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 5697 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*-----------------------------------------------------------*/
-// # 5802 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 5803 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*----------------------------------------------------------*/
-// # 5929 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 5930 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*-----------------------------------------------------------*/
 
 TickType_t uxTaskResetEventItemValue( void )
@@ -14388,7 +14523,7 @@ TickType_t uxTaskResetEventItemValue( void )
     {
         uint32_t ulReturn;
 
-        (__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5970, "uxIndexToWait < 1") : (void)0);
+        (__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 5971, "uxIndexToWait < 1") : (void)0);
 
         vTaskEnterCritical();
         {
@@ -14462,7 +14597,7 @@ TickType_t uxTaskResetEventItemValue( void )
     {
         BaseType_t xReturn;
 
-        (__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6044, "uxIndexToWait < 1") : (void)0);
+        (__builtin_expect(!(uxIndexToWait < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6045, "uxIndexToWait < 1") : (void)0);
 
         vTaskEnterCritical();
         {
@@ -14550,8 +14685,8 @@ TickType_t uxTaskResetEventItemValue( void )
         BaseType_t xReturn = ( ( ( char ) 1 ) );
         uint8_t ucOriginalNotifyState;
 
-        (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6132, "uxIndexToNotify < 1") : (void)0);
-        (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6133, "xTaskToNotify") : (void)0);
+        (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6133, "uxIndexToNotify < 1") : (void)0);
+        (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6134, "xTaskToNotify") : (void)0);
         pxTCB = xTaskToNotify;
 
         vTaskEnterCritical();
@@ -14604,7 +14739,7 @@ TickType_t uxTaskResetEventItemValue( void )
                     /* Should not get here if all enums are handled.
                      * Artificially force an assert by testing a value the
                      * compiler can't assume is const. */
-                    (__builtin_expect(!(xTickCount == ( TickType_t ) 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6186, "xTickCount == ( TickType_t ) 0") : (void)0);
+                    (__builtin_expect(!(xTickCount == ( TickType_t ) 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6187, "xTickCount == ( TickType_t ) 0") : (void)0);
 
                     break;
             }
@@ -14619,8 +14754,8 @@ TickType_t uxTaskResetEventItemValue( void )
                 ; { if( ( ( pxTCB )->uxPriority ) > uxTopReadyPriority ) { uxTopReadyPriority = ( ( pxTCB )->uxPriority ); } }; vListInsertEnd( &( pxReadyTasksLists[ ( pxTCB )->uxPriority ] ), &( ( pxTCB )->xStateListItem ) ); ;
 
                 /* The task should not have been on an event list. */
-                (__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6201, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0);
-// # 6220 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+                (__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6202, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0);
+// # 6221 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
                     {
                         prvYieldForTask( pxTCB, ( ( char ) 0 ) );
                     }
@@ -14653,8 +14788,8 @@ TickType_t uxTaskResetEventItemValue( void )
         BaseType_t xReturn = ( ( ( char ) 1 ) );
         UBaseType_t uxSavedInterruptStatus;
 
-        (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6252, "xTaskToNotify") : (void)0);
-        (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6253, "uxIndexToNotify < 1") : (void)0);
+        (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6253, "xTaskToNotify") : (void)0);
+        (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6254, "uxIndexToNotify < 1") : (void)0);
 
         /* RTOS ports that support interrupt nesting have the concept of a
          * maximum  system call (or maximum API call) interrupt priority.
@@ -14725,7 +14860,7 @@ TickType_t uxTaskResetEventItemValue( void )
                     /* Should not get here if all enums are handled.
                      * Artificially force an assert by testing a value the
                      * compiler can't assume is const. */
-                    (__builtin_expect(!(xTickCount == ( TickType_t ) 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6324, "xTickCount == ( TickType_t ) 0") : (void)0);
+                    (__builtin_expect(!(xTickCount == ( TickType_t ) 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6325, "xTickCount == ( TickType_t ) 0") : (void)0);
                     break;
             }
 
@@ -14736,7 +14871,7 @@ TickType_t uxTaskResetEventItemValue( void )
             if( ucOriginalNotifyState == ( ( uint8_t ) 1 ) )
             {
                 /* The task should not have been on an event list. */
-                (__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6335, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0);
+                (__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6336, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0);
 
                 if( uxSchedulerSuspended == ( UBaseType_t ) ( ( char ) 0 ) )
                 {
@@ -14781,8 +14916,8 @@ TickType_t uxTaskResetEventItemValue( void )
         uint8_t ucOriginalNotifyState;
         UBaseType_t uxSavedInterruptStatus;
 
-        (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6380, "xTaskToNotify") : (void)0);
-        (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6381, "uxIndexToNotify < 1") : (void)0);
+        (__builtin_expect(!(xTaskToNotify), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6381, "xTaskToNotify") : (void)0);
+        (__builtin_expect(!(uxIndexToNotify < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6382, "uxIndexToNotify < 1") : (void)0);
 
         /* RTOS ports that support interrupt nesting have the concept of a
          * maximum  system call (or maximum API call) interrupt priority.
@@ -14820,7 +14955,7 @@ TickType_t uxTaskResetEventItemValue( void )
             if( ucOriginalNotifyState == ( ( uint8_t ) 1 ) )
             {
                 /* The task should not have been on an event list. */
-                (__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6419, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0);
+                (__builtin_expect(!(( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6420, "( ( &( pxTCB->xEventListItem ) )->pxContainer ) == 0") : (void)0);
 
                 if( uxSchedulerSuspended == ( UBaseType_t ) ( ( char ) 0 ) )
                 {
@@ -14861,7 +14996,7 @@ TickType_t uxTaskResetEventItemValue( void )
         TCB_t * pxTCB;
         BaseType_t xReturn;
 
-        (__builtin_expect(!(uxIndexToClear < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6460, "uxIndexToClear < 1") : (void)0);
+        (__builtin_expect(!(uxIndexToClear < 1), 0) ? __assert_rtn ((const char *)-1L, "tasks.c", 6461, "uxIndexToClear < 1") : (void)0);
 
         /* If null is passed in here then it is the calling task that is having
          * its notification state cleared. */
@@ -14914,7 +15049,7 @@ TickType_t uxTaskResetEventItemValue( void )
 
 
 /*-----------------------------------------------------------*/
-// # 6529 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 6530 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 /*-----------------------------------------------------------*/
 
 static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait,
@@ -14990,7 +15125,7 @@ static void prvAddCurrentTaskToDelayedList( TickType_t xTicksToWait,
                 }
             }
         }
-// # 6641 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
+// # 6642 "/Users/reitobia/repos2/FreeRTOS-Kernel/tasks.c"
 }
 
 /* Code below here allows additional code to be inserted into this source file,
diff --git a/verification/verifast/proof/snippets/rp2040_port_c_snippets.c b/verification/verifast/proof/snippets/rp2040_port_c_snippets.c
index a86f657e1..000c7b966 100644
--- a/verification/verifast/proof/snippets/rp2040_port_c_snippets.c
+++ b/verification/verifast/proof/snippets/rp2040_port_c_snippets.c
@@ -46,6 +46,112 @@
     #define portTASK_RETURN_ADDRESS    prvTaskExitError
 #endif
 
+/*
+ * Setup the timer to generate the tick interrupts.  The implementation in this
+ * file is weak to allow application writers to change the timer used to
+ * generate the tick interrupt.
+ */
+void vPortSetupTimerInterrupt( void );
+
+/*
+ * Exception handlers.
+ */
+void xPortPendSVHandler( void ) __attribute__( ( naked ) );
+void xPortSysTickHandler( void );
+void vPortSVCHandler( void );
+
+/*
+ * Start first task is a separate function so it can be tested in isolation.
+ */
+static void vPortStartFirstTask( void ) __attribute__( ( naked ) );
+
+/*
+ * Used to catch tasks that attempt to return from their implementing function.
+ */
+static void prvTaskExitError( void );
+
+/*@
+// Represents a stack that grows down.
+predicate stack_p(StackType_t * pxStack, uint32_t ulStackDepth, StackType_t * pxTopOfStack, uint32_t freeCells) =
+	integers_(pxStack, sizeof(StackType_t), false, ulStackDepth, _) &*&
+    ulStackDepth > 0 &*&
+    freeCells >= 0 &*&
+    pxTopOfStack == pxStack + freeCells -1 &*&
+    0 <= freeCells &*& freeCells <= ulStackDepth;
+//	usedMem == pxStack - pxTopOfStack
+//	freeMem == ulStackDepth - usedMem
+	//freeCells * sizeof(StackType_t) == ulStackDepth * sizeof(StackType_t) - ((char*) pxStack - (char*) pxTopOfStack) &*&
+//	usedCells * sizeof(StackType_t) == ((char*) pxStack - (char*) pxTopOfStack);
+@*/
+
+/*/@
+lemma void split_stack(StackType_t * pxStack, int offset)
+requires stack_p(pxStack,?ulStackDepth, ?pxTopOfStack, ?freeMem, _) &*& 0 <= offset &*& 
+                offset * sizeof(StackType_t) < ulStackDepth;
+ensures integers_(pxStack, sizeof(StackType_t), true, offset * sizeof(StackType_t), _) &*&
+                integers_(pxStack + offset * sizeof(StackType_t), sizeof(StackType_t), true, ulStackDepth - offset * sizeof(StackType_t), _) ;
+{
+	open stack_p(_, _, _, _);
+	integers__split(pxStack, offset * sizeof(StackType_t) );
+}
+@*/
+
+/*@
+lemma void getTopOfStack(StackType_t* pxStack, StackType_t* pxTopOfStack)
+requires stack_p(pxStack,?ulStackDepth, pxTopOfStack, ?freeCells) &*&
+                 freeCells > 0;
+ensures // free cells minus top cell
+        integers_(pxStack, sizeof(StackType_t), false, freeCells-1, _)	&*&
+        // top stack cell
+		integer_(pxStack + freeCells-1, sizeof(StackType_t), false, _) &*&
+        // used stack cells
+		integers_(pxStack + freeCells, sizeof(StackType_t), false, 
+                  ulStackDepth - freeCells, _) &*&
+        // stack contraints necessary to close `stack_p` again
+        ulStackDepth > 0 &*&
+        freeCells >= 0 &*&
+        pxTopOfStack == pxStack + freeCells -1 &*&
+        0 <= freeCells &*& freeCells <= ulStackDepth;
+{
+    open stack_p(_, _, _, _);
+    integers__split(pxStack, freeCells-1);
+    open integers_(pxStack + (freeCells-1), _, _, _, _);
+}
+@*/
+
+
+// -------------------------------------------------
+// Validate stack predicate
+
+/* Simulates creation and initialisation of a stack that grows down as on RP2040.
+ */
+StackType_t* test_stack_pred(uint32_t depth)
+/*@ requires depth * sizeof(StackType_t) <= UINTPTR_MAX &*&
+             depth <= UINT_MAX &*&
+             depth > 0;
+ @*/
+/*@ ensures result == 0 ? true : stack_p(result, depth, ?top, depth) &*&
+            malloc_block_chars((char*) result, depth * sizeof(StackType_t));
+@*/
+{
+	StackType_t * stack;
+
+
+    /* Allocate space for the stack used by the task being created. */
+    stack = (StackType_t*) malloc( ( ( ( size_t ) depth ) * sizeof( StackType_t ) ) );
+    if(stack == 0) return 0;
+                
+    memset(stack, 0, (unsigned int ) depth * sizeof(StackType_t));
+                
+    StackType_t* top = stack + depth -1;
+           
+    //@ chars_to_integers_(stack, sizeof(StackType_t), false, depth); 
+    //@ close stack_p(stack, depth, top, depth);
+    // integers_(stack0, 4, false, depth, _)
+    return stack;
+}
+// -------------------------------------------------
+
 
 /*
  * See header file for description.
@@ -53,20 +159,43 @@
 StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack,
                                      TaskFunction_t pxCode,
                                      void * pvParameters )
-//@ requires true;
-//@ ensures true;
+/*@ requires pxTopOfStack > 0 &*&
+             stack_p(?pxStack, ?ulStackDepth, pxTopOfStack, ulStackDepth) &*&
+             ulStackDepth > 16;
+  @*/
+//@ ensures stack_p(pxStack, ulStackDepth, pxTopOfStack-16, ulStackDepth-16);
 {
+    //@ StackType_t* oldTop = pxTopOfStack;
+    //@ open stack_p(pxStack, ulStackDepth, pxTopOfStack, ulStackDepth);
+    ///@ close stack_p(pxStack, ulStackDepth, pxTopOfStack-1, ulStackDepth-1);
+    ///@ getTopOfStack(pxStack, pxTopOfStack-1);
+    //@ integers__split(pxStack, ulStackDepth-2);
+
     /* Simulate the stack frame as it would be created by a context switch
      * interrupt. */
     pxTopOfStack--;                                          /* Offset added to account for the way the MCU uses the stack on entry/exit of interrupts. */
     *pxTopOfStack = portINITIAL_XPSR;                        /* xPSR */
     pxTopOfStack--;
+    //@ close integers_(oldTop-1, sizeof(StackType_t), false, 2, _);
+    //@ integers__join(pxStack);
+    //@ ptr_range<void>(pxCode);
+    //@ integers__split(pxStack, ulStackDepth-3);
     *pxTopOfStack = ( StackType_t ) pxCode;                  /* PC */
+    //@ close integers_(oldTop-2, sizeof(StackType_t), false, 3, _);
     pxTopOfStack--;
+    //@ ptr_range<void>(prvTaskExitError);
+    //@ integers__join(pxStack);
+    //@ integers__split(pxStack, ulStackDepth-4);
     *pxTopOfStack = ( StackType_t ) portTASK_RETURN_ADDRESS; /* LR */
+    //@ close integers_(oldTop-3, sizeof(StackType_t), false, 4, _);
+    //@ integers__join(pxStack);
     pxTopOfStack -= 5;                                       /* R12, R3, R2 and R1. */
+    //@ ptr_range<void>(pvParameters);
+    //@ integers__split(pxStack, ulStackDepth-9);
     *pxTopOfStack = ( StackType_t ) pvParameters;            /* R0 */
+    //@ close integers_(oldTop-8, sizeof(StackType_t), false, 9, _);
+    //@ integers__join(pxStack);
     pxTopOfStack -= 8;                                       /* R11..R4. */
-
+    //@ close stack_p(pxStack, ulStackDepth, pxTopOfStack, ulStackDepth-16);
     return pxTopOfStack;
 }
\ No newline at end of file
diff --git a/verification/verifast/proof_setup/verifast_RP2040_axioms.h b/verification/verifast/proof_setup/verifast_RP2040_axioms.h
index 855727be5..cb9868587 100644
--- a/verification/verifast/proof_setup/verifast_RP2040_axioms.h
+++ b/verification/verifast/proof_setup/verifast_RP2040_axioms.h
@@ -10,7 +10,12 @@
 
 /*@
 // Axiomatizes that: 0 <= ptr <= 2^32 - 1
-lemma void uint32_t_ptr_range(uint32_t* ptr);
+//lemma void uint32_t_ptr_range(uint32_t* ptr);
+//requires true;
+//ensures 0 <= (int) ptr &*& (int) ptr <= 4294967295;
+
+// Axiomatizes that: 0 <= ptr <= 2^32 - 1
+lemma void ptr_range<t>(t* ptr);
 requires true;
 ensures 0 <= (int) ptr &*& (int) ptr <= 4294967295;
 @*/