Add the default definition of configPRECONDITION to FreeRTOS.h.

This is needed for CBMC proofs.

git-svn-id: https://svn.code.sf.net/p/freertos/code/trunk@2711 1d2547de-c912-0410-9cb9-b8ca96c0e9e2

diff --git a/FreeRTOS/Source/include/FreeRTOS.h b/FreeRTOS/Source/include/FreeRTOS.h
index 45c778a0396e29389b76109e0960c9ab916d08f6..14f98d0b0172fb6b689f8531b5c28b2dafae5c71 100644 (file)
--- a/FreeRTOS/Source/include/FreeRTOS.h
+++ b/FreeRTOS/Source/include/FreeRTOS.h
@@ -241,6 +241,19 @@ extern "C" {
        #define configASSERT_DEFINED 1\r
 #endif\r
 \r
+/* configPRECONDITION should resolve to configASSERT. The CBMC proofs need a way\r
+to track assumptions and assertions.\r
+- A configPRECONDITION statement should express an implicit invariant or\r
+assumption made.\r
+- A configASSERT statement should express an invariant that must hold explicit\r
+before calling the code. */\r
+#ifndef configPRECONDITION\r
+       #define configPRECONDITION( X ) configASSERT(X)\r
+       #define configPRECONDITION_DEFINED 0\r
+#else\r
+       #define configPRECONDITION_DEFINED 1\r
+#endif\r
+\r
 #ifndef portMEMORY_BARRIER\r
        #define portMEMORY_BARRIER()\r
 #endif\r