12 #ifndef CPROVER_CBMC_CBMC_PARSE_OPTIONS_H 13 #define CPROVER_CBMC_CBMC_PARSE_OPTIONS_H 28 #define CBMC_OPTIONS \ 29 "(program-only)(function):(preprocess)(slice-by-trace):" \ 30 "(no-simplify)(unwind):(unwindset):(slice-formula)(full-slice)" \ 31 "(debug-level):(no-propagation)(no-simplify-if)" \ 32 "(document-subgoals)(outfile):(test-preprocessor)" \ 33 "D:I:(c89)(c99)(c11)(cpp89)(cpp99)(cpp11)" \ 34 "(classpath):(cp):(main-class):" \ 35 "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \ 37 "(no-assertions)(no-assumptions)" \ 38 "(no-built-in-assertions)" \ 39 "(xml-ui)(xml-interface)(json-ui)" \ 40 "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \ 41 "(no-sat-preprocessor)" \ 42 "(no-pretty-names)(beautify)" \ 43 "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\ 44 "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ 45 "(little-endian)(big-endian)" \ 46 "(show-goto-functions)(show-loops)" \ 47 "(show-symbol-table)(show-parse-tree)(show-vcc)" \ 48 "(show-claims)(claim):(show-properties)" \ 49 "(drop-unused-functions)" \ 50 "(property):(stop-on-fail)(trace)" \ 51 "(error-label):(verbosity):(no-library)" \ 54 "(cover):(symex-coverage-report):" \ 56 "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \ 57 "(ppc-macos)(unsigned-char)" \ 58 "(arrays-uf-always)(arrays-uf-never)" \ 59 "(string-abstraction)(no-arch)(arch):" \ 60 "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \ 61 "(graphml-witness):" \ 62 "(java-max-vla-length):(java-unwind-enum-static)" \ 63 "(java-cp-include-files):" \ 64 "(localize-faults)(localize-faults-method):" \ 66 "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length) 74 virtual int doit()
override;
75 virtual void help()
override;
81 const std::string &extra_options);
115 #endif // CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
bool set_properties(goto_functionst &goto_functions)
virtual void get_command_line_options(optionst &options)
virtual int do_bmc(bmct &bmc, const goto_functionst &goto_functions)
invoke main modules
virtual bool process_goto_program(const optionst &options, goto_functionst &goto_functions)
virtual int get_modules(expr_listt &bmc_constraints)
std::list< exprt > expr_listt
virtual int doit() override
invoke main modules
virtual int get_goto_program(const optionst &options, expr_listt &bmc_constraints, goto_functionst &goto_functions)
cbmc_parse_optionst(int argc, const char **argv)
ui_message_handlert ui_message_handler
virtual void help() override
display command line help
virtual void register_languages()