cprover
jbmc_parse_options.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: JBMC Command Line Option Processing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_JBMC_JBMC_PARSE_OPTIONS_H
13 #define CPROVER_JBMC_JBMC_PARSE_OPTIONS_H
14 
15 #include <util/parse_options.h>
16 #include <util/timestamper.h>
17 #include <util/ui_message.h>
19 
20 #include <langapi/language.h>
21 
22 #include <analyses/goto_check.h>
23 
24 #include <goto-checker/bmc_util.h>
25 
29 
31 
33 
36 
37 #include <json/json_interface.h>
38 #include <xmllang/xml_interface.h>
39 
40 class goto_functionst;
41 class optionst;
42 
43 // clang-format off
44 #define JBMC_OPTIONS \
45  OPT_BMC \
46  "(preprocess)" \
47  OPT_FUNCTIONS \
48  "(no-simplify)(full-slice)" \
49  OPT_REACHABILITY_SLICER \
50  "(debug-level):(no-propagation)(no-simplify-if)" \
51  "(document-subgoals)(outfile):" \
52  "(object-bits):" \
53  "(classpath):(cp):" \
54  OPT_JAVA_JAR \
55  "(main-class):" \
56  OPT_JAVA_GOTO_BINARY \
57  "(no-assertions)(no-assumptions)" \
58  OPT_XML_INTERFACE \
59  OPT_JSON_INTERFACE \
60  "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
61  "(no-sat-preprocessor)" \
62  "(beautify)" \
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 \
68  "(show-loops)" \
69  "(show-symbol-table)" \
70  "(list-symbols)" \
71  "(show-parse-tree)" \
72  OPT_SHOW_PROPERTIES \
73  "(drop-unused-functions)" \
74  "(property):(stop-on-fail)(trace)" \
75  "(verbosity):" \
76  "(nondet-static)" \
77  OPT_JAVA_TRACE_VALIDATION \
78  "(version)" \
79  "(symex-coverage-report):" \
80  OPT_TIMESTAMP \
81  "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)" \
82  "(ppc-macos)" \
83  "(arrays-uf-always)(arrays-uf-never)" \
84  "(no-arch)(arch):" \
85  OPT_FLUSH \
86  JAVA_BYTECODE_LANGUAGE_OPTIONS \
87  "(java-unwind-enum-static)" \
88  "(localize-faults)" \
89  "(java-threading)" \
90  OPT_GOTO_TRACE \
91  OPT_VALIDATE \
92  "(symex-driven-lazy-loading)"
93 // clang-format on
94 
96 {
97 public:
98  virtual int doit() override;
99  virtual void help() override;
100 
101  jbmc_parse_optionst(int argc, const char **argv);
103  int argc,
104  const char **argv,
105  const std::string &extra_options);
106 
111  static void set_default_options(optionst &);
112 
114  goto_model_functiont &function,
115  const abstract_goto_modelt &,
116  const optionst &);
117  bool process_goto_functions(goto_modelt &goto_model, const optionst &options);
118 
119  bool can_generate_function_body(const irep_idt &name);
120 
122  const irep_idt &function_name,
123  symbol_table_baset &symbol_table,
124  goto_functiont &function,
125  bool body_available);
126 
127 protected:
130 
131  std::unique_ptr<class_hierarchyt> class_hierarchy;
132 
134  int get_goto_program(
135  std::unique_ptr<abstract_goto_modelt> &goto_model,
136  const optionst &);
137  bool show_loaded_functions(const abstract_goto_modelt &goto_model);
138  bool show_loaded_symbols(const abstract_goto_modelt &goto_model);
139 
144 };
145 
146 #endif // CPROVER_JBMC_JBMC_PARSE_OPTIONS_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
jbmc_parse_optionst::get_command_line_options
void get_command_line_options(optionst &)
Definition: jbmc_parse_options.cpp:122
parse_options_baset
Definition: parse_options.h:20
java_bytecode_language.h
jbmc_parse_optionst::process_goto_functions
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
Definition: jbmc_parse_options.cpp:906
optionst
Definition: options.h:23
json_interface.h
JSON Commandline Interface.
validation_interface.h
jbmc_parse_optionst::process_goto_function
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &, const optionst &)
Definition: jbmc_parse_options.cpp:769
goto_modelt
Definition: goto_model.h:26
jbmc_parse_optionst::generate_function_body
bool generate_function_body(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)
Definition: jbmc_parse_options.cpp:1007
jbmc_parse_optionst::object_factory_params
java_object_factory_parameterst object_factory_params
Definition: jbmc_parse_options.h:128
lazy_goto_model.h
Author: Diffblue Ltd.
path_storage.h
Storage of symbolic execution paths to resume.
jbmc_parse_optionst::stub_objects_are_not_null
bool stub_objects_are_not_null
Definition: jbmc_parse_options.h:129
goto_trace.h
Traces of GOTO Programs.
bmc_util.h
Bounded Model Checking Utilities.
jbmc_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: jbmc_parse_options.cpp:463
jbmc_parse_optionst::can_generate_function_body
bool can_generate_function_body(const irep_idt &name)
Definition: jbmc_parse_options.cpp:1000
jbmc_parse_optionst::show_loaded_symbols
bool show_loaded_symbols(const abstract_goto_modelt &goto_model)
Definition: jbmc_parse_options.cpp:857
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
show_properties.h
Show the properties.
jbmc_parse_optionst::class_hierarchy
std::unique_ptr< class_hierarchyt > class_hierarchy
Definition: jbmc_parse_options.h:131
language.h
Abstract interface to support a programming language.
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
string_refinement.h
String support via creating string constraints and progressively instantiating the universal constrai...
parse_options.h
goto_check.h
Program Transformation.
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
jbmc_parse_optionst::help
virtual void help() override
display command line help
Definition: jbmc_parse_options.cpp:1045
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
class_hierarchy.h
Class Hierarchy.
jbmc_parse_optionst::get_goto_program
int get_goto_program(std::unique_ptr< abstract_goto_modelt > &goto_model, const optionst &)
Definition: jbmc_parse_options.cpp:687
timestamper.h
Emit timestamps.
xml_interface.h
XML Interface.
jbmc_parse_optionst::set_default_options
static void set_default_options(optionst &)
Set the options that have default values.
Definition: jbmc_parse_options.cpp:102
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
jbmc_parse_optionst::jbmc_parse_optionst
jbmc_parse_optionst(int argc, const char **argv)
Definition: jbmc_parse_options.cpp:77
jbmc_parse_optionst::show_loaded_functions
bool show_loaded_functions(const abstract_goto_modelt &goto_model)
Definition: jbmc_parse_options.cpp:874
java_object_factory_parameterst
Definition: java_object_factory_parameters.h:16
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
jbmc_parse_optionst
Definition: jbmc_parse_options.h:96
ui_message.h
jbmc_parse_optionst::method_context
optionalt< prefix_filtert > method_context
See java_bytecode_languaget::method_context.
Definition: jbmc_parse_options.h:143