vTaskSwitchContexxt assumes that that interrupts have been deactivated.

This commit is contained in:
Tobias Reinhard 2022-11-15 08:28:21 -05:00
parent a7fdaca373
commit d2f10a6b25

16
tasks.c
View file

@ -4117,7 +4117,9 @@ void vTaskSwitchContext( BaseType_t xCoreID )
[?f_ISR]isrLock() &*& [?f_ISR]isrLock() &*&
[?f_task]taskLock() &*& [?f_task]taskLock() &*&
interruptState_p(xCoreID, ?state) &*& interruptState_p(xCoreID, ?state) &*&
xCoreID == coreID_f(); xCoreID == coreID_f() &*&
interruptsDisabled_f(state) == true &*&
coreLocalGlobalVars_p();
@*/ @*/
//@ ensures true; //@ ensures true;
{ {
@ -4132,6 +4134,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
portGET_TASK_LOCK(); /* Must always acquire the task lock first */ portGET_TASK_LOCK(); /* Must always acquire the task lock first */
portGET_ISR_LOCK(); portGET_ISR_LOCK();
//@ get_taskISRLockInv(); //@ get_taskISRLockInv();
//@ open coreLocalGlobalVars_p();
{ {
/* vTaskSwitchContext() must never be called from within a critical section. /* 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. */ * This is not necessarily true for vanilla FreeRTOS, but it is for this SMP port. */
@ -5268,8 +5271,15 @@ static void prvResetNextTaskUnblockTime( void )
#if ( ( INCLUDE_xTaskGetCurrentTaskHandle == 1 ) || ( configUSE_MUTEXES == 1 ) ) #if ( ( INCLUDE_xTaskGetCurrentTaskHandle == 1 ) || ( configUSE_MUTEXES == 1 ) )
TaskHandle_t xTaskGetCurrentTaskHandle( void ) TaskHandle_t xTaskGetCurrentTaskHandle( void )
//@ requires interruptState_p(?coreID, ?irpState); /*@ requires interruptState_p(coreID_f(), ?state) &*&
//@ ensures interruptState_p(coreID, irpState); 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;
@*/
{ {
TaskHandle_t xReturn; TaskHandle_t xReturn;
uint32_t ulState; uint32_t ulState;