From e629319b9f6988fae2f99cc9d51b40b06c9deca1 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Fri, 18 Nov 2022 09:32:24 -0500
Subject: [PATCH] Relaxed contract of `xTaskGetCurrentTaskHandle`.

---
 tasks.c | 2 --
 1 file changed, 2 deletions(-)

diff --git a/tasks.c b/tasks.c
index f32e5df24..8a1994eb2 100644
--- a/tasks.c
+++ b/tasks.c
@@ -5404,11 +5404,9 @@ static void prvResetNextTaskUnblockTime( void )
 
     TaskHandle_t xTaskGetCurrentTaskHandle( void )
     /*@ requires interruptState_p(coreID_f(), ?state) &*&
-             interruptsDisabled_f(state) == true &*&
              pointer(&pxCurrentTCBs[coreID_f], ?taskHandle);
      @*/
     /*@ ensures interruptState_p(coreID_f(), state) &*&
-             interruptsDisabled_f(state) == true &*&
              pointer(&pxCurrentTCBs[coreID_f], taskHandle) &*&
              result == taskHandle;
      @*/