#endif\r
\r
/* configPRECONDITION should be resolve to configASSERT.\r
- The CBMC proofs need a way to track assumptions and assertions.\r
- A configPRECONDITION statement should express an implicit invariant or assumption made.\r
- A configASSERT statement should express an invariant that must hold explicit before calling\r
- the code. */\r
+The CBMC proofs need a way to track assumptions and assertions.\r
+A configPRECONDITION statement should express an implicit invariant or\r
+assumption made. A configASSERT statement should express an invariant that must\r
+hold explicit before calling the code. */\r
#ifndef configPRECONDITION\r
#define configPRECONDITION( X ) configASSERT(X)\r
#define configPRECONDITION_DEFINED 0\r