len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-11 22:25:14 -05:00
Code Issues Projects Releases Packages Wiki Activity

Deleted proof annotations in prvAddNewTaskToReadyList

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-13 10:24:21 -05:00
parent 676e9fddad
commit de64106012
1 changed files with 0 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

5
Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
View file

@ -2139,11 +2139,6 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
/*-----------------------------------------------------------*/ /*-----------------------------------------------------------*/
static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB ) 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 /* Ensure interrupts don't access the task lists while the lists are being
* updated. */ * updated. */