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

Strengthened postcondition of reordering lemma.

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

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

@ -285,7 +285,8 @@ void VF_reordeReadyList(List_t* pxReadyList, ListItem_t * pxTaskItem)
readyLists_p(?gReorderedCellLists, ?gReorderedOwnerLists) &*& readyLists_p(?gReorderedCellLists, ?gReorderedOwnerLists) &*&
length(gReorderedCellLists) == length(gCellLists) &*& length(gReorderedCellLists) == length(gCellLists) &*&
length(gReorderedOwnerLists) == length(gOwnerLists) &*& length(gReorderedOwnerLists) == length(gOwnerLists) &*&
length(gReorderedCellLists) == length(gReorderedOwnerLists); length(gReorderedCellLists) == length(gReorderedOwnerLists) &*&
forall(gReorderedOwnerLists, (superset)(gTasks)) == true;
@*/ @*/
{ {
//@ open VF_reordeReadyList__ghost_args(_, _, _, _); //@ open VF_reordeReadyList__ghost_args(_, _, _, _);