1 files changed, 12 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/stubs/cbmc.c b/FreeRTOS-Plus/Test/CBMC/stubs/cbmc.c
new file mode 100644
index 000000000..73ad21893
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/stubs/cbmc.c
@@ -0,0 +1,12 @@
+#include "cbmc.h"
+
+/****************************************************************
+ * Model a malloc that can fail (CBMC malloc does not fail) and
+ * check that CBMC can model an object of the requested size.
+ ****************************************************************/
+
+void * safeMalloc( size_t size )
+{
+    __CPROVER_assert( size < CBMC_MAX_OBJECT_SIZE, "safeMalloc size too big" );
+    return nondet_bool() ? NULL : malloc( size );
+}