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

Started to define predicates encapsulating access permissions to global variables.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-04 14:22:11 -04:00
parent ac798f9fb5
commit 25dda73ef9
1 changed files with 25 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2,26 +2,36 @@
#define VERIFAST_LOCK_PREDICATES_H #define VERIFAST_LOCK_PREDICATES_H
/* We assume that macros evaluate as follows:
* - `configMAX_PRIORITIES` -> 32
*/
/*@ /*@
predicate tasks_global_vars() = // We assume tha `configNUM_CORES` evaluates to 1.
// Lists for ready and blocked tasks. // TODO: Parametrise in terms of `configNUM_CORES`.
//chars((char*) pxReadyTasksLists, 32 * sizeof(List_t), _) &*& // PROBLEM: Shouldn't `configNUM_CORES` be greater than 1?
//chars((char*) xDelayedTaskList1) &*& predicate otherGlobalVars() =
integer_(&uxCurrentNumberOfTasks, sizeof(UBaseType_t), false, _)
// Other file private variables. --------------------------------
integer_((void*) uxCurrentNumberOfTasks, sizeof(UBaseType_t), false, _)
&*& &*&
integer_(&xTickCount, sizeof(TickType_t), false, _)
&*&
integer_(&uxTopReadyPriority, sizeof(UBaseType_t), false, _)
&*&
integer_(&xSchedulerRunning, sizeof(BaseType_t), true, _)
&*&
integer_(&xPendedTicks, sizeof(TickType_t), false, _)
&*&
integers_(&xYieldPendings, sizeof(BaseType_t), true, 1, _)
&*&
integer_(&uxTaskNumber, sizeof(UBaseType_t), false, _)
&*&
integer_(&xNextTaskUnblockTime, sizeof(TickType_t), false, _)
&*&
pointers(&xIdleTaskHandle, 1, _);
predicate unprotectedGlobalVars() =
true; [_] integer_(&xSchedulerRunning, sizeof(BaseType_t), true, _);
@*/ @*/
/*
void vf_validate_lock_predicaet() void vf_validate_lock_predicate()
//@ requires module(tasks__pp, true); //@ requires module(tasks__pp, true);
//@ ensures true; //@ ensures true;
{ {
@ -30,5 +40,6 @@ void vf_validate_lock_predicaet()
//@ close tasks_global_vars(); //@ close tasks_global_vars();
} }
*/
#endif /* VERIFAST_LOCK_PREDICATES_H */ #endif /* VERIFAST_LOCK_PREDICATES_H */