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

Removed deprecated predicates and proofs.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-13 10:46:51 -05:00
parent 1672d293ab
commit ff763690a4
1 changed files with 0 additions and 49 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -34,55 +34,6 @@ predicate unalignedRestOfStack_p(char* p, uint32_t ulUnalignedBytes) =
chars(p, ulUnalignedBytes, _); chars(p, ulUnalignedBytes, _);
@*/ @*/
/*@
// Represents a stack that grows down (cf. RP2040 stack)
predicate stack_p(StackType_t * pxStack, uint32_t ulStackDepth, StackType_t * pxTopOfStack, uint32_t freeCells) =
integers_(pxStack, sizeof(StackType_t), false, ulStackDepth, _) &*&
ulStackDepth > 0 &*&
freeCells >= 0 &*&
pxTopOfStack == pxStack + freeCells -1 &*&
0 <= freeCells &*& freeCells <= ulStackDepth;
// usedMem == pxStack - pxTopOfStack
// freeMem == ulStackDepth - usedMem
//freeCells * sizeof(StackType_t) == ulStackDepth * sizeof(StackType_t) - ((char*) pxStack - (char*) pxTopOfStack) &*&
// usedCells * sizeof(StackType_t) == ((char*) pxStack - (char*) pxTopOfStack);
@*/
/*/@
lemma void split_stack(StackType_t * pxStack, int offset)
requires stack_p(pxStack,?ulStackDepth, ?pxTopOfStack, ?freeMem, _) &*& 0 <= offset &*&
offset * sizeof(StackType_t) < ulStackDepth;
ensures integers_(pxStack, sizeof(StackType_t), true, offset * sizeof(StackType_t), _) &*&
integers_(pxStack + offset * sizeof(StackType_t), sizeof(StackType_t), true, ulStackDepth - offset * sizeof(StackType_t), _) ;
{
open stack_p(_, _, _, _);
integers__split(pxStack, offset * sizeof(StackType_t) );
}
@*/
/*@
// TODO: Do we need this lemma or is it usually cleaner to split stack manually?
lemma void getTopOfStack(StackType_t* pxStack, StackType_t* pxTopOfStack)
requires stack_p(pxStack,?ulStackDepth, pxTopOfStack, ?freeCells) &*&
freeCells > 0;
ensures // free cells minus top cell
integers_(pxStack, sizeof(StackType_t), false, freeCells-1, _) &*&
// top stack cell
integer_(pxStack + freeCells-1, sizeof(StackType_t), false, _) &*&
// used stack cells
integers_(pxStack + freeCells, sizeof(StackType_t), false,
ulStackDepth - freeCells, _) &*&
// stack contraints necessary to close `stack_p` again
ulStackDepth > 0 &*&
freeCells >= 0 &*&
pxTopOfStack == pxStack + freeCells -1 &*&
0 <= freeCells &*& freeCells <= ulStackDepth;
{
open stack_p(_, _, _, _);
integers__split(pxStack, freeCells-1);
open integers_(pxStack + (freeCells-1), _, _, _, _);
}
@*/
#endif /* STACK_PREDICATES */ #endif /* STACK_PREDICATES */