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

taskCHECK_FOR_STACK_OVERFLOW assumes minimal stack size. Updated stack predicate accordingly.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-16 15:30:40 -05:00
parent 7675b3bbe4
commit 383a055872
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -24,7 +24,11 @@ predicate stack_p_2(StackType_t * pxStack,
integers_(pxTopOfStack + 1, sizeof(StackType_t), false, ulUsedCells, _) &*& integers_(pxTopOfStack + 1, sizeof(StackType_t), false, ulUsedCells, _) &*&
// Unaligned rest // Unaligned rest
unalignedRestOfStack_p((char*) pxStack + ulFreeBytes + sizeof(StackType_t) * ulUsedCells, unalignedRestOfStack_p((char*) pxStack + ulFreeBytes + sizeof(StackType_t) * ulUsedCells,
ulUnalignedBytes); ulUnalignedBytes) &*&
// `taskCHECK_FOR_STACK_OVERFLOW` macro on RP2040 port expects minimal stack size
ulFreeBytes >= 0 &*&
ulUsedCells >= 0 &*&
ulFreeBytes + ulUsedCells * sizeof(StackType_t) >= 3 * sizeof(StackType_t);
predicate unalignedRestOfStack_p(char* p, uint32_t ulUnalignedBytes) = predicate unalignedRestOfStack_p(char* p, uint32_t ulUnalignedBytes) =
chars(p, ulUnalignedBytes, _); chars(p, ulUnalignedBytes, _);