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

Renamed predicate stack_p_2 into stack_p

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-13 10:57:41 -05:00
parent 3675aa6011
commit 677ffa8cea
3 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

8
Test/VeriFast/tasks/vTaskSwitchContext/include/stack_macros.h
View file

@ -112,10 +112,10 @@
@*/ \ @*/ \
{ \ { \
/*@ open prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/ \ /*@ open prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/ \
/*@ assert( stack_p_2(?pxStack, ?ulStackDepth, ?pxTopOfStack, \ /*@ assert( stack_p(?pxStack, ?ulStackDepth, ?pxTopOfStack, \
?ulFreeBytes, ?ulUsedCells, ?ulUnalignedBytes) ); \ ?ulFreeBytes, ?ulUsedCells, ?ulUnalignedBytes) ); \
@*/ \ @*/ \
/*@ open stack_p_2(_, _, _, _, _, _); @*/ \ /*@ open stack_p(_, _, _, _, _, _); @*/ \
/* The detour below allows us to skip proving that `ulFreeBytes` \ /* The detour below allows us to skip proving that `ulFreeBytes` \
* is a multiple of `sizeof(StackType_t)`. \ * is a multiple of `sizeof(StackType_t)`. \
*/ \ */ \
@ -136,7 +136,7 @@
/*@ integers__to_chars(pxStack); @*/ \ /*@ integers__to_chars(pxStack); @*/ \
/*@ chars_join((char*) pxStack); @*/ \ /*@ chars_join((char*) pxStack); @*/ \
/*@ chars_split((char*) pxStack, ulFreeBytesOnStack); @*/ \ /*@ chars_split((char*) pxStack, ulFreeBytesOnStack); @*/ \
/*@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, \ /*@ close stack_p(pxStack, ulStackDepth, pxTopOfStack, \
ulFreeBytes, ulUsedCells, ulUnalignedBytes); \ ulFreeBytes, ulUsedCells, ulUnalignedBytes); \
@*/ \ @*/ \
/*@ close prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/ \ /*@ close prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/ \
@ -149,7 +149,7 @@
integers__to_chars(pxStack); \ integers__to_chars(pxStack); \
chars_join((char*) pxStack); \ chars_join((char*) pxStack); \
chars_split((char*) pxStack, ulFreeBytesOnStack); \ chars_split((char*) pxStack, ulFreeBytesOnStack); \
close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, \ close stack_p(pxStack, ulStackDepth, pxTopOfStack, \
ulFreeBytes, ulUsedCells, ulUnalignedBytes); \ ulFreeBytes, ulUsedCells, ulUnalignedBytes); \
close prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); \ close prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); \
} \ } \

2
Test/VeriFast/tasks/vTaskSwitchContext/proof/stack_predicates.h
View file

@ -4,7 +4,7 @@
/*@ /*@
// Represents a stack that grows down (cf. RP2040 stack) // Represents a stack that grows down (cf. RP2040 stack)
predicate stack_p_2(StackType_t * pxStack, predicate stack_p(StackType_t * pxStack,
uint32_t ulStackDepth, uint32_t ulStackDepth,
StackType_t * pxTopOfStack, StackType_t * pxTopOfStack,
uint32_t ulFreeBytes, uint32_t ulFreeBytes,

4
Test/VeriFast/tasks/vTaskSwitchContext/proof/task_predicates.h
View file

@ -15,7 +15,7 @@ predicate TCB_p(TCB_t * tcb, uint32_t ulFreeBytesOnStack) =
malloc_block_tskTaskControlBlock(tcb) &*& malloc_block_tskTaskControlBlock(tcb) &*&
tcb->pxStack |-> ?stackPtr &*& tcb->pxStack |-> ?stackPtr &*&
tcb->pxTopOfStack |-> ?topPtr &*& tcb->pxTopOfStack |-> ?topPtr &*&
stack_p_2(stackPtr, ?ulStackDepth, topPtr, stack_p(stackPtr, ?ulStackDepth, topPtr,
ulFreeBytesOnStack, ?ulUsedCells, ?ulUnalignedBytes) &*& ulFreeBytesOnStack, ?ulUsedCells, ?ulUnalignedBytes) &*&
xLIST_ITEM(&tcb->xStateListItem, _, _, _, _, _) &*& xLIST_ITEM(&tcb->xStateListItem, _, _, _, _, _) &*&
@ -63,7 +63,7 @@ predicate TCB_p(TCB_t * tcb, uint32_t ulFreeBytesOnStack) =
predicate prvSeg_TCB_p(TCB_t* tcb, uint32_t ulFreeBytesOnStack) = predicate prvSeg_TCB_p(TCB_t* tcb, uint32_t ulFreeBytesOnStack) =
tcb->pxStack |-> ?stackPtr &*& tcb->pxStack |-> ?stackPtr &*&
tcb->pxTopOfStack |-> ?topPtr &*& tcb->pxTopOfStack |-> ?topPtr &*&
stack_p_2(stackPtr, ?ulStackDepth, topPtr, stack_p(stackPtr, ?ulStackDepth, topPtr,
ulFreeBytesOnStack, ?ulUsedCells, ?ulUnalignedBytes); ulFreeBytesOnStack, ?ulUsedCells, ?ulUnalignedBytes);
// This predicate represents a shared part of a TCB that can be accessed by // This predicate represents a shared part of a TCB that can be accessed by