validate.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Goto program validation macros
 
Author: Daniel Poetzl
 
\*******************************************************************/
 
#ifndef CPROVER_UTIL_VALIDATE_H
#define CPROVER_UTIL_VALIDATE_H
 
#include <type_traits>
 
#include "exception_utils.h"
#include "validation_mode.h"
 
#define DATA_CHECK(vm, condition, message)                                     \
  do                                                                           \
  {                                                                            \
    switch(vm)                                                                 \
    {                                                                          \
    case validation_modet::INVARIANT:                                          \
      DATA_INVARIANT(condition, message);                                      \
      break;                                                                   \
    case validation_modet::EXCEPTION:                                          \
      if(!(condition))                                                         \
        throw incorrect_goto_program_exceptiont(message);                      \
      break;                                                                   \
    }                                                                          \
  } while(0)
#define DATA_CHECK(vm, condition, message)                                     \ …
 
#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message, ...)               \
  do                                                                           \
  {                                                                            \
    switch(vm)                                                                 \
    {                                                                          \
    case validation_modet::INVARIANT:                                          \
      DATA_INVARIANT_WITH_DIAGNOSTICS(condition, message, __VA_ARGS__);        \
      break;                                                                   \
    case validation_modet::EXCEPTION:                                          \
      if(!(condition))                                                         \
        throw incorrect_goto_program_exceptiont(message, __VA_ARGS__);         \
      break;                                                                   \
    }                                                                          \
  } while(0)
#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message, ...)               \ …
 
#endif /* CPROVER_UTIL_VALIDATE_H */