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

Introduced predicates to differentiate between public and private parts of a TCB.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-16 10:55:25 -05:00
parent 360afe4374
commit dbf03a0ab2
1 changed files with 15 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -93,4 +93,19 @@ predicate absTCB_p(TCB_t* tcb) =
TCB_p(tcb, _); TCB_p(tcb, _);
@*/ @*/
/*@
// We have to segment TCBs into:
// (i) public parts that can be accessed by anyone after
// following the appropriote synchronization steps and
// (ii) private parts that may only be used by the task itself
// which the TCB represents
//
// The predicates below will be expanded iteratively.
predicate prvTCB_p(TCB_t* tcb, uint32_t ulFreeBytesOnStack);
predicate pubTCB_p(TCB_t* tcb) =
tcb->uxCriticalNesting |-> ?uxCriticalNesting;
@*/
#endif /* TASKS_GH */ #endif /* TASKS_GH */