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

Added TODO

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-18 16:47:47 -05:00
parent cf65065a0c
commit 5b6a92f023
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -42,14 +42,12 @@ ensures List_array_p(array, index) &*&
close List_array_p(array, index); close List_array_p(array, index);
} }
} }
// For testing purposes only!
// TODO: Replace by Aaloks list predicate
predicate List_p(List_t* l);
@*/ @*/
/*@ /*@
// TODO: We know that the list of priority 0 is never empty.
// It contains the idle task and nothing else.
predicate readyLists_p() = predicate readyLists_p() =
List_array_p(&pxReadyTasksLists, configMAX_PRIORITIES); List_array_p(&pxReadyTasksLists, configMAX_PRIORITIES);
@*/ @*/