|
|
|
@ -241,12 +241,11 @@ 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. */
|
|
|
|
|
/* configPRECONDITION should be 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
|
|
|
|
|