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

Refined task control block predicate TCB_p such that it can be used to justify memset-ing the stack.

Browse source
This commit is contained in:
Tobias Reinhard 2022-10-25 13:22:10 -04:00
parent 80134a65ed
commit 1042ea8cf8
3 changed files with 15 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

2
tasks.c
View file

@ -1361,7 +1361,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
pxNewTCB->pxStack = pxStack; pxNewTCB->pxStack = pxStack;
//@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _); //@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _);
//@ close xLIST_ITEM(&pxNewTCB->xEventListItem, _, _, _, _); //@ close xLIST_ITEM(&pxNewTCB->xEventListItem, _, _, _, _);
//@ close TCB_p(pxNewTCB); //@ close TCB_p(pxNewTCB, ((size_t) usStackDepth) * sizeof(StackType_t));
} }
else else
{ {

10
verification/verifast/preprocessed_files/tasks--pp.c
View file

@ -81,7 +81,7 @@ predicate xLIST_ITEM(
/*@ /*@
// This predicate represents the memory corresponding to an // This predicate represents the memory corresponding to an
// instance of type `TCB_t` aka `tskTaskControlBlock`. // instance of type `TCB_t` aka `tskTaskControlBlock`.
predicate TCB_p(TCB_t * tcb) = predicate TCB_p(TCB_t * tcb, int stackSize) =
malloc_block_tskTaskControlBlock(tcb) &*& malloc_block_tskTaskControlBlock(tcb) &*&
tcb->pxTopOfStack |-> _ &*& tcb->pxTopOfStack |-> _ &*&
@ -91,7 +91,11 @@ predicate TCB_p(TCB_t * tcb) =
struct_xLIST_ITEM_padding(&tcb->xEventListItem) &*& struct_xLIST_ITEM_padding(&tcb->xEventListItem) &*&
tcb->uxPriority |-> _ &*& tcb->uxPriority |-> _ &*&
tcb->pxStack |-> _ &*&
tcb->pxStack |-> ?stackPtr &*&
chars_((char*) stackPtr, stackSize, _) &*&
malloc_block_chars((char*) stackPtr, stackSize) &*&
tcb->xTaskRunState |-> _ &*& tcb->xTaskRunState |-> _ &*&
tcb->xIsIdle |-> _ &*& tcb->xIsIdle |-> _ &*&
@ -10723,7 +10727,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
pxNewTCB->pxStack = pxStack; pxNewTCB->pxStack = pxStack;
//@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _); //@ close xLIST_ITEM(&pxNewTCB->xStateListItem, _, _, _, _);
//@ close xLIST_ITEM(&pxNewTCB->xEventListItem, _, _, _, _); //@ close xLIST_ITEM(&pxNewTCB->xEventListItem, _, _, _, _);
//@ close TCB_p(pxNewTCB); //@ close TCB_p(pxNewTCB, ((size_t) usStackDepth) * sizeof(StackType_t));
} }
else else
{ {

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

@ -8,7 +8,7 @@
/*@ /*@
// This predicate represents the memory corresponding to an // This predicate represents the memory corresponding to an
// instance of type `TCB_t` aka `tskTaskControlBlock`. // instance of type `TCB_t` aka `tskTaskControlBlock`.
predicate TCB_p(TCB_t * tcb) = predicate TCB_p(TCB_t * tcb, int stackSize) =
malloc_block_tskTaskControlBlock(tcb) &*& malloc_block_tskTaskControlBlock(tcb) &*&
tcb->pxTopOfStack |-> _ &*& tcb->pxTopOfStack |-> _ &*&
@ -18,7 +18,11 @@ predicate TCB_p(TCB_t * tcb) =
struct_xLIST_ITEM_padding(&tcb->xEventListItem) &*& struct_xLIST_ITEM_padding(&tcb->xEventListItem) &*&
tcb->uxPriority |-> _ &*& tcb->uxPriority |-> _ &*&
tcb->pxStack |-> _ &*&
tcb->pxStack |-> ?stackPtr &*&
chars_((char*) stackPtr, stackSize, _) &*&
malloc_block_chars((char*) stackPtr, stackSize) &*&
tcb->xTaskRunState |-> _ &*& tcb->xTaskRunState |-> _ &*&
tcb->xIsIdle |-> _ &*& tcb->xIsIdle |-> _ &*&