summaryrefslogtreecommitdiff
path: root/FreeRTOS/Test/CBMC/include/tasksStubs.h
diff options
context:
space:
mode:
Diffstat (limited to 'FreeRTOS/Test/CBMC/include/tasksStubs.h')
-rw-r--r--FreeRTOS/Test/CBMC/include/tasksStubs.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/FreeRTOS/Test/CBMC/include/tasksStubs.h b/FreeRTOS/Test/CBMC/include/tasksStubs.h
index a0dd6de4a..e50a5cad1 100644
--- a/FreeRTOS/Test/CBMC/include/tasksStubs.h
+++ b/FreeRTOS/Test/CBMC/include/tasksStubs.h
@@ -5,6 +5,7 @@
#include "task.h"
BaseType_t xState;
-void vInitTaskCheckForTimeOut(BaseType_t maxCounter, BaseType_t maxCounter_limit);
+void vInitTaskCheckForTimeOut( BaseType_t maxCounter,
+ BaseType_t maxCounter_limit );
#endif /* INC_TASK_STUBS_H */