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

Deleted deprecated predicate and lemmas.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-02 15:05:20 -05:00
parent df780a1823
commit b44eb855d9
1 changed files with 0 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -143,44 +143,6 @@ predicate exists_in_taskISRLockInv_p(list<void*> gTasks) =
fixpoint bool mem_list_elem<t>(list<t> xs, t x) { fixpoint bool mem_list_elem<t>(list<t> xs, t x) {
return mem(x, xs); return mem(x, xs);
} }
// l ∈ taskLists. ∀t ∈ tasks. sharedSeg_TCB_p(t)
predicate valid_sharedSeg_TCBs_p(list<list<void*> > taskLists) =
foreach(taskLists, foreach_sharedSeg_TCB_p);
// ∀t ∈ tasks. sharedSeg_TCB_p(t)
predicate foreach_sharedSeg_TCB_p(list<void*> tasks) =
foreach(tasks, sharedSeg_TCB_p);
lemma void open_valid_sharedSeg_TCBs(list<list<void*> > taskLists,
list<void*> tasks)
requires
valid_sharedSeg_TCBs_p(taskLists) &*&
mem(tasks, taskLists) == true;
ensures
valid_sharedSeg_TCBs_p(remove(tasks, taskLists)) &*&
foreach(tasks, sharedSeg_TCB_p);
{
open valid_sharedSeg_TCBs_p(taskLists);
foreach_remove(tasks, taskLists);
close valid_sharedSeg_TCBs_p(remove(tasks, taskLists));
open foreach_sharedSeg_TCB_p(tasks);
}
lemma void close_valid_sharedSeg_TCBs(list<list<void*> > taskLists,
list<void*> tasks)
requires
valid_sharedSeg_TCBs_p(remove(tasks, taskLists)) &*&
foreach(tasks, sharedSeg_TCB_p) &*&
mem(tasks, taskLists) == true;
ensures
valid_sharedSeg_TCBs_p(taskLists);
{
close foreach_sharedSeg_TCB_p(tasks);
open valid_sharedSeg_TCBs_p(remove(tasks, taskLists));
foreach_unremove(tasks, taskLists);
close valid_sharedSeg_TCBs_p(taskLists);
}
@*/ @*/
/* /*