Go to the documentation of this file. 9 #ifndef CPROVER_UTIL_VALIDATE_H 10 #define CPROVER_UTIL_VALIDATE_H 12 #include <type_traits> 22 #define DATA_CHECK(vm, condition, message) \ 27 case validation_modet::INVARIANT: \ 28 DATA_INVARIANT(condition, message); \ 30 case validation_modet::EXCEPTION: \ 32 throw incorrect_goto_program_exceptiont(message); \ 37 #define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message, ...) \ 42 case validation_modet::INVARIANT: \ 43 DATA_INVARIANT_WITH_DIAGNOSTICS(condition, message, __VA_ARGS__); \ 45 case validation_modet::EXCEPTION: \ 47 throw incorrect_goto_program_exceptiont(message, __VA_ARGS__); \