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

Refined precondition of reordering lemma.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-06 09:53:35 -05:00
parent 7fe2ec22f2
commit e68b45969b
1 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -279,7 +279,7 @@ void VF_reordeReadyList(List_t* pxReadyList, ListItem_t * pxTaskItem)
gPrefOwnerLists == take(gOffset, gOwnerLists) &*& gPrefOwnerLists == take(gOffset, gOwnerLists) &*&
gSufOwnerLists == drop(gOffset+1, gOwnerLists) &*& gSufOwnerLists == drop(gOffset+1, gOwnerLists) &*&
forall(gOwnerLists, (superset)(gTasks)) == true &*& forall(gOwnerLists, (superset)(gTasks)) == true &*&
forall(gOwners, (mem_list_elem)(gTasks)) == true; subset(gOwners, gTasks) == true;
@*/ @*/
/*@ ensures /*@ ensures
readyLists_p(?gReorderedCellLists, ?gReorderedOwnerLists) &*& readyLists_p(?gReorderedCellLists, ?gReorderedOwnerLists) &*&
@ -291,6 +291,12 @@ void VF_reordeReadyList(List_t* pxReadyList, ListItem_t * pxTaskItem)
{ {
//@ open VF_reordeReadyList__ghost_args(_, _, _, _); //@ open VF_reordeReadyList__ghost_args(_, _, _, _);
// Proving `∀o ∈ gOwners. o ∈ gTasks`
//@ forall_mem(gOwners, gOwnerLists, (superset)(gTasks));
//@ assert( superset(gTasks, gOwners) == true );
//@ subset_implies_forall_mem(gOwners, gTasks);
//@ assert( forall(gOwners, (mem_list_elem)(gTasks)) == true );
// Proving `length(gCells) == length(gOwners) == gSize + 1`: // Proving `length(gCells) == length(gOwners) == gSize + 1`:
//@ open xLIST(pxReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners); //@ open xLIST(pxReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners);
//@ close xLIST(pxReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners); //@ close xLIST(pxReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners);