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 
34 
35 #include <json/json_interface.h>
36 #include <xmllang/xml_interface.h>
37 
38 class goto_functiont;
40 class optionst;
41 
42 // clang-format off
43 #define JBMC_OPTIONS \
44  OPT_BMC \
45  "(preprocess)" \
46  OPT_FUNCTIONS \
47  "(no-simplify)(full-slice)" \
48  OPT_REACHABILITY_SLICER \
49  "(debug-level):(no-propagation)(no-simplify-if)" \
50  "(document-subgoals)(outfile):" \
51  "(object-bits):" \
52  "(classpath):(cp):" \
53  OPT_JAVA_JAR \
54  "(main-class):" \
55  OPT_JAVA_GOTO_BINARY \
56  "(no-assertions)(no-assumptions)" \
57  OPT_XML_INTERFACE \
58  OPT_JSON_INTERFACE \
59  "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
60  "(no-sat-preprocessor)" \
61  "(beautify)" \
62  "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
63  OPT_STRING_REFINEMENT \
64  "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
65  OPT_SHOW_GOTO_FUNCTIONS \
66  OPT_SHOW_CLASS_HIERARCHY \
67  "(show-loops)" \
68  "(show-symbol-table)" \
69  "(list-symbols)" \
70  "(show-parse-tree)" \
71  OPT_SHOW_PROPERTIES \
72  "(drop-unused-functions)" \
73  "(property):(stop-on-fail)(trace)" \
74  "(verbosity):" \
75  "(nondet-static)" \
76  OPT_JAVA_TRACE_VALIDATION \
77  "(version)" \
78  "(symex-coverage-report):" \
79  OPT_TIMESTAMP \
80  "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)" \
81  "(ppc-macos)" \
82  "(arrays-uf-always)(arrays-uf-never)" \
83  "(no-arch)(arch):" \
84  OPT_FLUSH \
85  JAVA_BYTECODE_LANGUAGE_OPTIONS \
86  "(java-unwind-enum-static)" \
87  "(localize-faults)" \
88  "(java-threading)" \
89  OPT_GOTO_TRACE \
90  OPT_VALIDATE \
91  "(symex-driven-lazy-loading)"
92 // clang-format on
93 
95 {
96 public:
97  virtual int doit() override;
98  virtual void help() override;
99 
100  jbmc_parse_optionst(int argc, const char **argv);
102  int argc,
103  const char **argv,
104  const std::string &extra_options);
105 
110  static void set_default_options(optionst &);
111 
113  goto_model_functiont &function,
114  const abstract_goto_modelt &,
115  const optionst &);
116  bool process_goto_functions(goto_modelt &goto_model, const optionst &options);
117 
118  bool can_generate_function_body(const irep_idt &name);
119 
121  const irep_idt &function_name,
122  symbol_table_baset &symbol_table,
123  goto_functiont &function,
124  bool body_available);
125 
126 protected:
129 
130  std::unique_ptr<class_hierarchyt> class_hierarchy;
131 
133  int get_goto_program(
134  std::unique_ptr<abstract_goto_modelt> &goto_model,
135  const optionst &);
136  bool show_loaded_functions(const abstract_goto_modelt &goto_model);
137  bool show_loaded_symbols(const abstract_goto_modelt &goto_model);
138 
143 };
144 
145 #endif // CPROVER_JBMC_JBMC_PARSE_OPTIONS_H
Bounded Model Checking Utilities.
Class Hierarchy.
Abstract interface to eager or lazy GOTO models.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
bool show_loaded_functions(const abstract_goto_modelt &goto_model)
void get_command_line_options(optionst &)
bool can_generate_function_body(const irep_idt &name)
std::unique_ptr< class_hierarchyt > class_hierarchy
bool show_loaded_symbols(const abstract_goto_modelt &goto_model)
virtual int doit() override
invoke main modules
virtual void help() override
display command line help
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &, const optionst &)
java_object_factory_parameterst object_factory_params
bool process_goto_functions(goto_modelt &goto_model, const optionst &options)
optionalt< prefix_filtert > method_context
See java_bytecode_languaget::method_context.
int get_goto_program(std::unique_ptr< abstract_goto_modelt > &goto_model, const optionst &)
jbmc_parse_optionst(int argc, const char **argv)
bool generate_function_body(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)
static void set_default_options(optionst &)
Set the options that have default values.
The symbol table base class interface.
Program Transformation.
Traces of GOTO Programs.
JSON Commandline Interface.
Abstract interface to support a programming language.
nonstd::optional< T > optionalt
Definition: optional.h:35
Show the properties.
String support via creating string constraints and progressively instantiating the universal constrai...
Emit timestamps.
XML Interface.