len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-04-20 05:21:59 -04:00
Code Issues Packages Projects Releases Wiki Activity

Add the default definition of configPRECONDITION to FreeRTOS.h.

Browse source 
This is needed for CBMC proofs.
This commit is contained in:
Gaurav Aggarwal 2019-07-27 23:03:23 +00:00
parent b4c06085e1
commit 6bad7d2055
1 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
FreeRTOS/Source/include/FreeRTOS.h
View file

@ -241,6 +241,19 @@ extern "C" {
#define configASSERT_DEFINED 1 #define configASSERT_DEFINED 1
#endif #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 #ifndef portMEMORY_BARRIER
#define portMEMORY_BARRIER() #define portMEMORY_BARRIER()
#endif #endif