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

Verified new contract for xTaskGetCurrentTaskHandle.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-17 12:08:38 -05:00
parent 63a8d73ecc
commit fb01980b63
2 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

4
tasks.c
View file

@ -895,7 +895,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
static BaseType_t prvSelectHighestPriorityTask( const BaseType_t xCoreID )
//@ requires true;
//@ assert true;
//@ ensures true;
{
UBaseType_t uxCurrentPriority = uxTopReadyPriority;
BaseType_t xTaskScheduled = pdFALSE;
@ -5353,9 +5353,7 @@ static void prvResetNextTaskUnblockTime( void )
uint32_t ulState;
ulState = portDISABLE_INTERRUPTS();
//@ open coreLocalInterruptInv_p();
xReturn = pxCurrentTCBs[ portGET_CORE_ID() ];
//@ close coreLocalInterruptInv_p();
portRESTORE_INTERRUPTS( ulState );
return xReturn;

6
verification/verifast/proof/verifast_port_contracts.h
View file

@ -35,14 +35,16 @@ uint32_t VF__portDISABLE_INTERRUPTS();
/*@ ensures result == state &*&
interruptState_p(coreID, ?newState) &*&
interruptsDisabled_f(newState) == true &*&
coreLocalInterruptInv_p();
interruptsDisabled_f(state) == true
? newState == state
: coreLocalInterruptInv_p();
@*/
#undef portRESTORE_INTERRUPTS
#define portRESTORE_INTERRUPTS(ulState) VF__portRESTORE_INTERRUPTS(ulState)
void VF__portRESTORE_INTERRUPTS(uint32_t ulState);
/*@ requires interruptState_p(?coreID, ?tmpState) &*&
interruptsDisabled_f(tmpState) == true
(interruptsDisabled_f(tmpState) == true && interruptsDisabled_f(ulState) == false)
? coreLocalInterruptInv_p()
: true;
@*/