CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
validation_interface.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto program validation common command line options
4
5Author: Daniel Poetzl
6
7\*******************************************************************/
8
9#ifndef CPROVER_UTIL_VALIDATION_INTERFACE_H
10#define CPROVER_UTIL_VALIDATION_INTERFACE_H
11
12#define OPT_VALIDATE \
13 "(validate-goto-model)" \
14 "(validate-ssa-equation)"
15
16#define HELP_VALIDATE \
17 " {y--validate-goto-model} \t " \
18 "enable additional well-formedness checks on the goto program\n" \
19 " {y--validate-ssa-equation} \t " \
20 "enable additional well-formedness checks on the SSA representation\n"
21
22#endif /* CPROVER_UTIL_VALIDATION_INTERFACE_H */