Go to the documentation of this file.
12 #ifndef CPROVER_JBMC_JBMC_PARSE_OPTIONS_H
13 #define CPROVER_JBMC_JBMC_PARSE_OPTIONS_H
44 #define JBMC_OPTIONS \
48 "(no-simplify)(full-slice)" \
49 OPT_REACHABILITY_SLICER \
50 "(debug-level):(no-propagation)(no-simplify-if)" \
51 "(document-subgoals)(outfile):" \
56 OPT_JAVA_GOTO_BINARY \
57 "(no-assertions)(no-assumptions)" \
60 "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
61 "(no-sat-preprocessor)" \
63 "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
64 OPT_STRING_REFINEMENT \
65 "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
66 OPT_SHOW_GOTO_FUNCTIONS \
67 OPT_SHOW_CLASS_HIERARCHY \
69 "(show-symbol-table)" \
73 "(drop-unused-functions)" \
74 "(property):(stop-on-fail)(trace)" \
77 OPT_JAVA_TRACE_VALIDATION \
79 "(symex-coverage-report):" \
81 "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)" \
83 "(arrays-uf-always)(arrays-uf-never)" \
86 JAVA_BYTECODE_LANGUAGE_OPTIONS \
87 "(java-unwind-enum-static)" \
92 "(symex-driven-lazy-loading)"
98 virtual int doit()
override;
99 virtual void help()
override;
105 const std::string &extra_options);
125 bool body_available);
135 std::unique_ptr<abstract_goto_modelt> &goto_model,
146 #endif // CPROVER_JBMC_JBMC_PARSE_OPTIONS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void get_command_line_options(optionst &)
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
JSON Commandline Interface.
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &, const optionst &)
bool generate_function_body(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)
java_object_factory_parameterst object_factory_params
Storage of symbolic execution paths to resume.
bool stub_objects_are_not_null
Bounded Model Checking Utilities.
virtual int doit() override
invoke main modules
bool can_generate_function_body(const irep_idt &name)
bool show_loaded_symbols(const abstract_goto_modelt &goto_model)
The symbol table base class interface.
std::unique_ptr< class_hierarchyt > class_hierarchy
Abstract interface to support a programming language.
A goto function, consisting of function type (see type), function body (see body),...
String support via creating string constraints and progressively instantiating the universal constrai...
nonstd::optional< T > optionalt
virtual void help() override
display command line help
A collection of goto functions.
int get_goto_program(std::unique_ptr< abstract_goto_modelt > &goto_model, const optionst &)
static void set_default_options(optionst &)
Set the options that have default values.
Abstract interface to eager or lazy GOTO models.
jbmc_parse_optionst(int argc, const char **argv)
bool show_loaded_functions(const abstract_goto_modelt &goto_model)
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
optionalt< prefix_filtert > method_context
See java_bytecode_languaget::method_context.