CBMC
|
Go to the source code of this file.
Macros | |
#define | DATA_CHECK(vm, condition, message) |
This macro takes a condition which denotes a well-formedness criterion on goto programs, expressions, instructions, etc. More... | |
#define | DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message, ...) |
#define DATA_CHECK | ( | vm, | |
condition, | |||
message | |||
) |
This macro takes a condition which denotes a well-formedness criterion on goto programs, expressions, instructions, etc.
The first parameter should be of type validate_modet
and indicates whether DATA_INVARIANT() is used to check the condition, or if an exception is thrown when the condition does not hold.
Definition at line 22 of file validate.h.
#define DATA_CHECK_WITH_DIAGNOSTICS | ( | vm, | |
condition, | |||
message, | |||
... | |||
) |
Definition at line 37 of file validate.h.