1 #include "FreeRTOS.h"
2 #include "task.h"
3 #include "tasksStubs.h"
4 
5 #ifndef TASK_STUB_COUNTER
6     #define TASK_STUB_COUNTER    0;
7 #endif
8 
9 /* 5 is a magic number, but we need some number here as a default value.
10  * This value is used to bound any loop depending on xTaskCheckForTimeOut
11  * as a loop bound. It should be overwritten in the Makefile.json adapting
12  * to the performance requirements of the harness. */
13 #ifndef TASK_STUB_COUNTER_LIMIT
14     #define TASK_STUB_COUNTER_LIMIT    5;
15 #endif
16 
17 
18 static BaseType_t xCounter = TASK_STUB_COUNTER;
19 static BaseType_t xCounterLimit = TASK_STUB_COUNTER_LIMIT;
20 
xTaskGetSchedulerState(void)21 BaseType_t xTaskGetSchedulerState( void )
22 {
23     return xState;
24 }
25 
26 
27 /* This function is another method apart from overwriting the defines to init the max
28  * loop bound. */
vInitTaskCheckForTimeOut(BaseType_t maxCounter,BaseType_t maxCounter_limit)29 void vInitTaskCheckForTimeOut( BaseType_t maxCounter,
30                                BaseType_t maxCounter_limit )
31 {
32     xCounter = maxCounter;
33     xCounterLimit = maxCounter_limit;
34 }
35 
36 /* This is mostly called in a loop. For CBMC, we have to bound the loop
37  * to a max limits of calls. Therefore this Stub models a nondet timeout in
38  * max TASK_STUB_COUNTER_LIMIT iterations.*/
xTaskCheckForTimeOut(TimeOut_t * const pxTimeOut,TickType_t * const pxTicksToWait)39 BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut,
40                                  TickType_t * const pxTicksToWait )
41 {
42     ++xCounter;
43 
44     if( xCounter == xCounterLimit )
45     {
46         return pdTRUE;
47     }
48     else
49     {
50         return nondet_basetype();
51     }
52 }
53