12 #ifndef CPROVER_JBMC_JBMC_PARSE_OPTIONS_H 13 #define CPROVER_JBMC_JBMC_PARSE_OPTIONS_H 40 #define JBMC_OPTIONS \ 42 "(preprocess)(slice-by-trace):" \ 44 "(no-simplify)(full-slice)" \ 45 OPT_REACHABILITY_SLICER \ 46 "(debug-level):(no-propagation)(no-simplify-if)" \ 47 "(document-subgoals)(outfile):" \ 49 "(classpath):(cp):(main-class):" \ 51 "(no-assertions)(no-assumptions)" \ 52 "(no-built-in-assertions)" \ 54 "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \ 55 "(no-sat-preprocessor)" \ 57 "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\ 59 "(string-printable)" \ 60 "(string-max-length):" \ 61 "(string-max-input-length):" \ 62 "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ 63 OPT_SHOW_GOTO_FUNCTIONS \ 64 OPT_SHOW_CLASS_HIERARCHY \ 66 "(show-symbol-table)(show-parse-tree)" \ 68 "(drop-unused-functions)" \ 69 "(property):(stop-on-fail)(trace)" \ 72 "(cover):(symex-coverage-report):" \ 74 "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)" \ 76 "(arrays-uf-always)(arrays-uf-never)" \ 79 JAVA_BYTECODE_LANGUAGE_OPTIONS \ 80 "(java-unwind-enum-static)" \ 81 "(localize-faults)(localize-faults-method):" \ 84 "(symex-driven-lazy-loading)" 92 virtual int doit()
override;
93 virtual void help()
override;
99 const std::string &extra_options);
113 bool body_available);
124 std::unique_ptr<goto_modelt> &goto_model,
const optionst &);
130 #endif // CPROVER_JBMC_JBMC_PARSE_OPTIONS_H bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
jbmc_parse_optionst(int argc, const char **argv)
Abstract interface to eager or lazy GOTO models.
object_factory_parameterst object_factory_params
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &, const optionst &)
std::unique_ptr< cover_configt > cover_config
Factory and information for path_storaget.
path_strategy_choosert path_strategy_chooser
bool generate_function_body(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)
bool can_generate_function_body(const irep_idt &name)
Abstract interface to support a programming language.
virtual int doit() override
invoke main modules
virtual void help() override
display command line help
int get_goto_program(std::unique_ptr< goto_modelt > &goto_model, const optionst &)
bool show_loaded_functions(const abstract_goto_modelt &goto_model)
Bounded Model Checking for ANSI-C + HDL.
bool stub_objects_are_not_null
bool set_properties(goto_modelt &goto_model)
The symbol table base class interface.
Bounded model checking or path exploration for goto-programs.
ui_message_handlert ui_message_handler
void get_command_line_options(optionst &)
Coverage Instrumentation.
Storage of symbolic execution paths to resume.
Interface providing access to a single function in a GOTO model, plus its associated symbol table...