12 #ifndef CPROVER_CBMC_CBMC_PARSE_OPTIONS_H 13 #define CPROVER_CBMC_CBMC_PARSE_OPTIONS_H 41 #define CBMC_OPTIONS \ 43 "(preprocess)(slice-by-trace):" \ 45 "(no-simplify)(full-slice)" \ 46 OPT_REACHABILITY_SLICER \ 47 "(debug-level):(no-propagation)(no-simplify-if)" \ 48 "(document-subgoals)(outfile):(test-preprocessor)" \ 49 "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \ 52 "(no-assertions)(no-assumptions)" \ 53 "(xml-ui)(xml-interface)(json-ui)" \ 54 "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \ 56 "(no-sat-preprocessor)" \ 58 "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\ 59 OPT_STRING_REFINEMENT_CBMC \ 60 "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ 61 "(little-endian)(big-endian)" \ 62 OPT_SHOW_GOTO_FUNCTIONS \ 64 "(show-symbol-table)(show-parse-tree)" \ 65 "(drop-unused-functions)" \ 66 "(property):(stop-on-fail)(trace)" \ 67 "(error-label):(verbosity):(no-library)" \ 70 "(cover):(symex-coverage-report):" \ 73 "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \ 74 "(ppc-macos)(unsigned-char)" \ 75 "(arrays-uf-always)(arrays-uf-never)" \ 76 "(string-abstraction)(no-arch)(arch):" \ 77 "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \ 79 "(localize-faults)(localize-faults-method):" \ 83 "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length) 92 virtual int doit()
override;
93 virtual void help()
override;
99 const std::string &extra_options);
127 #endif // CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
void get_command_line_options(optionst &)
static int get_goto_program(goto_modelt &, const optionst &, const cmdlinet &, messaget &, ui_message_handlert &)
const path_strategy_choosert path_strategy_chooser
Factory and information for path_storaget.
static bool process_goto_program(goto_modelt &, const optionst &, messaget &)
void preprocessing(const optionst &)
Abstract interface to support a programming language.
A collection of goto functions.
Class that provides messages with a built-in verbosity 'level'.
String support via creating string constraints and progressively instantiating the universal constrai...
virtual int doit() override
invoke main modules
static void set_default_options(optionst &)
Set the options that have default values.
Bounded Model Checking for ANSI-C + HDL.
cbmc_parse_optionst(int argc, const char **argv)
Bounded model checking or path exploration for goto-programs.
ui_message_handlert ui_message_handler
virtual void help() override
display command line help
void register_languages()