CBMC
validate.h File Reference
#include <type_traits>
#include "exception_utils.h"
#include "validation_mode.h"
+ Include dependency graph for validate.h:
+ This graph shows which files directly or indirectly include this file:

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, ...)
 

Macro Definition Documentation

◆ DATA_CHECK

#define DATA_CHECK (   vm,
  condition,
  message 
)
Value:
do \
{ \
switch(vm) \
{ \
DATA_INVARIANT(condition, message); \
break; \
if(!(condition)) \
break; \
} \
} while(0)
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...

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.

◆ DATA_CHECK_WITH_DIAGNOSTICS

#define DATA_CHECK_WITH_DIAGNOSTICS (   vm,
  condition,
  message,
  ... 
)
Value:
do \
{ \
switch(vm) \
{ \
DATA_INVARIANT_WITH_DIAGNOSTICS(condition, message, __VA_ARGS__); \
break; \
if(!(condition)) \
throw incorrect_goto_program_exceptiont(message, __VA_ARGS__); \
break; \
} \
} while(0)

Definition at line 37 of file validate.h.