CBMC
validation_interface.h File Reference
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros

#define OPT_VALIDATE
 
#define HELP_VALIDATE
 

Macro Definition Documentation

◆ HELP_VALIDATE

#define HELP_VALIDATE
Value:
" {y--validate-goto-model} \t " \
"enable additional well-formedness checks on the goto program\n" \
" {y--validate-ssa-equation} \t " \
"enable additional well-formedness checks on the SSA representation\n"

Definition at line 16 of file validation_interface.h.

◆ OPT_VALIDATE

#define OPT_VALIDATE
Value:
"(validate-goto-model)" \
"(validate-ssa-equation)"

Definition at line 12 of file validation_interface.h.