CBMC
Loading...
Searching...
No Matches
Macros
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.
 
#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)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
@ INVARIANT
@ EXCEPTION

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) \
{ \
break; \
if(!(condition)) \
break; \
} \
} while(0)

Definition at line 37 of file validate.h.

AltStyle によって変換されたページ (->オリジナル) /