From: gaurav-aws <gaurav-aws@1d2547de-c912-0410-9cb9-b8ca96c0e9e2>
Date: Sat, 27 Jul 2019 23:03:23 +0000 (+0000)
Subject: Add the default definition of configPRECONDITION to FreeRTOS.h.
X-Git-Tag: V10.3.0~112
X-Git-Url: https://git.sur5r.net/?a=commitdiff_plain;h=68d64b6a7908b1025826bcef0f108a17a92e6a5f;p=freertos

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 45c778a03..14f98d0b0 100644
--- a/FreeRTOS/Source/include/FreeRTOS.h
+++ b/FreeRTOS/Source/include/FreeRTOS.h
@@ -241,6 +241,19 @@ extern "C" {
 	#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