diff options
Diffstat (limited to 'FreeRTOS/Test/CBMC/proofs/Task/TaskGetSchedulerState/tasks_test_access_functions.h')
| -rw-r--r-- | FreeRTOS/Test/CBMC/proofs/Task/TaskGetSchedulerState/tasks_test_access_functions.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskGetSchedulerState/tasks_test_access_functions.h b/FreeRTOS/Test/CBMC/proofs/Task/TaskGetSchedulerState/tasks_test_access_functions.h index 7e1b29489..31181374a 100644 --- a/FreeRTOS/Test/CBMC/proofs/Task/TaskGetSchedulerState/tasks_test_access_functions.h +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskGetSchedulerState/tasks_test_access_functions.h @@ -32,6 +32,6 @@ */ void vSetGlobalVariables( void ) { - xSchedulerRunning = nondet_basetype(); - uxSchedulerSuspended = nondet_ubasetype(); + xSchedulerRunning = nondet_basetype(); + uxSchedulerSuspended = nondet_ubasetype(); } |