12 #ifndef CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
13 #define CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
44 #define CBMC_OPTIONS \
46 "(preprocess)(slice-by-trace):" \
48 "(no-simplify)(full-slice)" \
49 OPT_REACHABILITY_SLICER \
50 "(debug-level):(no-propagation)(no-simplify-if)" \
51 "(document-subgoals)(outfile):(test-preprocessor)" \
52 "(write-solver-stats-to):" \
53 "(show-array-constraints)" \
61 "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
63 "(external-sat-solver):" \
64 "(no-sat-preprocessor)" \
66 "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
67 OPT_STRING_REFINEMENT_CBMC \
68 OPT_SHOW_GOTO_FUNCTIONS \
70 "(show-symbol-table)(show-parse-tree)" \
71 "(drop-unused-functions)" \
72 "(havoc-undefined-functions)" \
73 "(property):(stop-on-fail)(trace)" \
74 "(verbosity):(no-library)" \
78 "(symex-coverage-report):" \
81 "(arrays-uf-always)(arrays-uf-never)" \
87 "(claim):(show-claims)(floatbv)(all-claims)(all-properties)"
93 virtual int doit()
override;
94 virtual void help()
override;
100 const std::string &extra_options);
Bounded Model Checking Utilities.
virtual int doit() override
invoke main modules
static bool process_goto_program(goto_modelt &, const optionst &, messaget &)
static void set_default_options(optionst &)
Set the options that have default values.
static int get_goto_program(goto_modelt &, const optionst &, const cmdlinet &, ui_message_handlert &)
void get_command_line_options(optionst &)
void preprocessing(const optionst &)
virtual void help() override
display command line help
void register_languages()
cbmc_parse_optionst(int argc, const char **argv)
A collection of goto functions.
Class that provides messages with a built-in verbosity 'level'.
Coverage Instrumentation.
JSON Commandline Interface.
Abstract interface to support a programming language.
String support via creating string constraints and progressively instantiating the universal constrai...