1 files changed, 47 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.c b/FreeRTOS-Plus/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.c
new file mode 100644
index 000000000..3fe245f80
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.c
@@ -0,0 +1,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();
+	}
+}