CBMC
validate.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto program validation macros
4 
5 Author: Daniel Poetzl
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_VALIDATE_H
10 #define CPROVER_UTIL_VALIDATE_H
11 
12 #include <type_traits>
13 
14 #include "exception_utils.h"
15 #include "validation_mode.h"
16 
22 #define DATA_CHECK(vm, condition, message) \
23  do \
24  { \
25  switch(vm) \
26  { \
27  case validation_modet::INVARIANT: \
28  DATA_INVARIANT(condition, message); \
29  break; \
30  case validation_modet::EXCEPTION: \
31  if(!(condition)) \
32  throw incorrect_goto_program_exceptiont(message); \
33  break; \
34  } \
35  } while(0)
36 
37 #define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message, ...) \
38  do \
39  { \
40  switch(vm) \
41  { \
42  case validation_modet::INVARIANT: \
43  DATA_INVARIANT_WITH_DIAGNOSTICS(condition, message, __VA_ARGS__); \
44  break; \
45  case validation_modet::EXCEPTION: \
46  if(!(condition)) \
47  throw incorrect_goto_program_exceptiont(message, __VA_ARGS__); \
48  break; \
49  } \
50  } while(0)
51 
52 #endif /* CPROVER_UTIL_VALIDATE_H */