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