diff options
Diffstat (limited to 'FreeRTOS-Plus/Test/CBMC/include/tasksStubs.h')
| -rw-r--r-- | FreeRTOS-Plus/Test/CBMC/include/tasksStubs.h | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/include/tasksStubs.h b/FreeRTOS-Plus/Test/CBMC/include/tasksStubs.h new file mode 100644 index 000000000..a0dd6de4a --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/include/tasksStubs.h @@ -0,0 +1,10 @@ +#ifndef INC_TASK_STUBS_H +#define INC_TASK_STUBS_H + +#include "FreeRTOS.h" +#include "task.h" + +BaseType_t xState; +void vInitTaskCheckForTimeOut(BaseType_t maxCounter, BaseType_t maxCounter_limit); + +#endif /* INC_TASK_STUBS_H */ |