File tree 1 file changed +5
-6
lines changed
1 file changed +5
-6
lines changed Original file line number Diff line number Diff line change @@ -241,12 +241,11 @@ extern "C" {
241
241
#define configASSERT_DEFINED 1
242
242
#endif
243
243
244
- /* configPRECONDITION should resolve to configASSERT. The CBMC proofs need a way
245
- to track assumptions and assertions.
246
- - A configPRECONDITION statement should express an implicit invariant or
247
- assumption made.
248
- - A configASSERT statement should express an invariant that must hold explicit
249
- before calling the code. */
244
+ /* configPRECONDITION should be resolve to configASSERT.
245
+ The CBMC proofs need a way to track assumptions and assertions.
246
+ A configPRECONDITION statement should express an implicit invariant or assumption made.
247
+ A configASSERT statement should express an invariant that must hold explicit before calling
248
+ the code. */
250
249
#ifndef configPRECONDITION
251
250
#define configPRECONDITION ( X ) configASSERT(X)
252
251
#define configPRECONDITION_DEFINED 0
You can’t perform that action at this time.
0 commit comments