From de64106012032380e4bc6c3246fca4113aa91bcd Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Tue, 13 Dec 2022 10:24:21 -0500
Subject: [PATCH] Deleted proof annotations in `prvAddNewTaskToReadyList`

---
 Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
index ef12b6819..e5ff0b1b0 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
@@ -2139,11 +2139,6 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
 /*-----------------------------------------------------------*/
 
 static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
-/*//@ requires interruptState_p(?coreID, _) &*&
-             unprotectedGlobalVars(); 
-  @*/
-/*//@ ensures true; 
-  @*/
 {
     /* Ensure interrupts don't access the task lists while the lists are being
      * updated. */