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

Deleted deprecated lemmas and predicates.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-02 15:07:43 -05:00
parent 3be9d76d82
commit 1919f8142f
1 changed files with 0 additions and 36 deletions
Download patch file Download diff file Expand all files Collapse all files

36
verification/verifast/proof/verifast_lock_predicates.h
View file

@ -145,42 +145,6 @@ fixpoint bool mem_list_elem<t>(list<t> xs, t x) {
} }
@*/ @*/
/*
foreach(itemLists, foreach_sharedSeg_TCB_of_itemOwner);
// Auxiliary prediactes to express nested quantification
// ∀gCells ∈ gCellLists. ∀item ∈ gCells. sharedSeg_TCB_p(item->pvOwner)
// TODO: Can we refactor this to make easier to understand?
// We cannot acces `item->pvOwner` without the necessary points-to chunk.
// TODO: Expose list of owners in ITEM and DLS predicates.
predicate sharedSeg_TCB_of_itemOwner(struct xLIST_ITEM* item) =
sharedSeg_TCB_p(item->pvOwner);
predicate foreach_sharedSeg_TCB_of_itemOwner(list<struct xLIST_ITEM*> items) =
foreach(items, sharedSeg_TCB_of_itemOwner);
lemma void open_collection_of_sharedSeg_TCB(list<list<struct xLIST_ITEM*> > itemLists,
list<struct xLIST_ITEM*> items)
requires
collection_of_sharedSeg_TCB_p(itemLists) &*&
mem(items, itemLists) == true;
ensures
collection_of_sharedSeg_TCB_p(remove(items, itemLists)) &*&
foreach(items, sharedSeg_TCB_of_itemOwner);
{
open collection_of_sharedSeg_TCB_p(itemLists);
foreach_remove(items, itemLists);
open foreach_sharedSeg_TCB_of_itemOwner(items);
close collection_of_sharedSeg_TCB_p(remove(items, itemLists));
}
// TODO: Add closing lemma
@*/