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

vTaskSwitchContext now has access to the current task's stack.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-16 15:31:49 -05:00
parent 383a055872
commit c3c350f8dc
2 changed files with 23 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

23
tasks.c
View file

@ -4128,28 +4128,37 @@ BaseType_t xTaskIncrementTick( void )
void vTaskSwitchContext( BaseType_t xCoreID ) void vTaskSwitchContext( BaseType_t xCoreID )
/*@ requires 0 <= xCoreID &*& xCoreID < configNUM_CORES &*& /*@ requires 0 <= xCoreID &*& xCoreID < configNUM_CORES &*&
xCoreID == coreID_f() &*& xCoreID == coreID_f()
&*&
// access to locks and disabled interrupts // access to locks and disabled interrupts
locked(nil) &*& locked(nil) &*&
[?f_ISR]isrLock() &*& [?f_ISR]isrLock() &*&
[?f_task]taskLock() &*& [?f_task]taskLock() &*&
interruptState_p(xCoreID, ?state) &*& interruptState_p(xCoreID, ?state) &*&
interruptsDisabled_f(state) == true &*& interruptsDisabled_f(state) == true
&*&
// opened predicate `coreLocalInterruptInv_p()` // opened predicate `coreLocalInterruptInv_p()`
pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*&
pubTCB_p(gCurrentTCB, 0) &*& pubTCB_p(gCurrentTCB, 0) &*&
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _); integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _)
&*&
// read access to current task's stack pointer, etc
prvTCB_p(gCurrentTCB, ?ulFreeBytesOnStack);
@*/ @*/
/*@ ensures // all locks release and interrupts remain disabled /*@ ensures // all locks release and interrupts remain disabled
locked(nil) &*& locked(nil) &*&
[f_ISR]isrLock() &*& [f_ISR]isrLock() &*&
[f_task]taskLock() &*& [f_task]taskLock() &*&
interruptState_p(xCoreID, state) &*& interruptState_p(xCoreID, state)
&*&
// opened predicate `coreLocalInterruptInv_p()` // opened predicate `coreLocalInterruptInv_p()`
pointer(&pxCurrentTCBs[coreID_f], ?gNewCurrentTCB) &*& pointer(&pxCurrentTCBs[coreID_f], ?gNewCurrentTCB) &*&
pubTCB_p(gNewCurrentTCB, 0) &*& pubTCB_p(gNewCurrentTCB, 0) &*&
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _); integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _)
&*&
// read access to current task's stack pointer, etc
prvTCB_p(gCurrentTCB, ulFreeBytesOnStack);
// Remark: the part of the post condition relating to TCBs will have to change. // Remark: the part of the post condition relating to TCBs will have to change.
@*/ @*/
{ {
@ -4229,6 +4238,10 @@ void vTaskSwitchContext( BaseType_t xCoreID )
#endif /* configGENERATE_RUN_TIME_STATS */ #endif /* configGENERATE_RUN_TIME_STATS */
/* Check for stack overflow, if configured. */ /* Check for stack overflow, if configured. */
//@ open prvTCB_p(gCurrentTCB, ulFreeBytesOnStack);
//@ assert( stack_p_2(?pxStack, ?ulStackDepth, ?pxTopOfStack, ?ulFreeBytes, ?ulUsedCells, ?ulUnalignedBytes) );
//@ open stack_p_2(pxStack, _, _, _, _, _);
//@ assert(ulFreeBytes + ulUsedCells >= 3 * sizeof(StackType_t) );
taskCHECK_FOR_STACK_OVERFLOW(); taskCHECK_FOR_STACK_OVERFLOW();
/* Before the currently running task is switched out, save its errno. */ /* Before the currently running task is switched out, save its errno. */

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

@ -102,7 +102,11 @@ predicate absTCB_p(TCB_t* tcb) =
// //
// The predicates below will be expanded iteratively. // The predicates below will be expanded iteratively.
predicate prvTCB_p(TCB_t* tcb, uint32_t ulFreeBytesOnStack); predicate prvTCB_p(TCB_t* tcb, uint32_t ulFreeBytesOnStack) =
tcb->pxStack |-> ?stackPtr &*&
tcb->pxTopOfStack |-> ?topPtr &*&
stack_p_2(stackPtr, ?ulStackDepth, topPtr,
ulFreeBytesOnStack, ?ulUsedCells, ?ulUnalignedBytes);
predicate pubTCB_p(TCB_t* tcb, UBaseType_t uxCriticalNesting) = predicate pubTCB_p(TCB_t* tcb, UBaseType_t uxCriticalNesting) =
tcb->uxCriticalNesting |-> uxCriticalNesting; tcb->uxCriticalNesting |-> uxCriticalNesting;