Add the default definition of configPRECONDITION to FreeRTOS.h.
This is needed for CBMC proofs.
diff --git a/FreeRTOS/Source/include/FreeRTOS.h b/FreeRTOS/Source/include/FreeRTOS.h
index 45c778a..14f98d0 100644
--- a/FreeRTOS/Source/include/FreeRTOS.h
+++ b/FreeRTOS/Source/include/FreeRTOS.h
@@ -241,6 +241,19 @@
#define configASSERT_DEFINED 1
#endif
+/* configPRECONDITION should resolve to configASSERT. The CBMC proofs need a way
+to track assumptions and assertions.
+- A configPRECONDITION statement should express an implicit invariant or
+assumption made.
+- A configASSERT statement should express an invariant that must hold explicit
+before calling the code. */
+#ifndef configPRECONDITION
+ #define configPRECONDITION( X ) configASSERT(X)
+ #define configPRECONDITION_DEFINED 0
+#else
+ #define configPRECONDITION_DEFINED 1
+#endif
+
#ifndef portMEMORY_BARRIER
#define portMEMORY_BARRIER()
#endif
