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/ui_message.h>
16 #include <util/parse_options.h>
17 #include <util/timestamper.h>
18 
19 #include <langapi/language.h>
20 
21 #include <analyses/goto_check.h>
22 
23 #include <cbmc/bmc.h>
24 
29 
31 
33 
35 
36 class bmct;
37 class goto_functionst;
38 class optionst;
39 
40 // clang-format off
41 #define JBMC_OPTIONS \
42  OPT_BMC \
43  "(preprocess)(slice-by-trace):" \
44  OPT_FUNCTIONS \
45  "(no-simplify)(full-slice)" \
46  OPT_REACHABILITY_SLICER \
47  "(debug-level):(no-propagation)(no-simplify-if)" \
48  "(document-subgoals)(outfile):" \
49  "(object-bits):" \
50  "(classpath):(cp):(main-class):" \
51  "(no-assertions)(no-assumptions)" \
52  "(xml-ui)(json-ui)" \
53  "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
54  "(no-sat-preprocessor)" \
55  "(beautify)" \
56  "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
57  OPT_STRING_REFINEMENT \
58  "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
59  OPT_SHOW_GOTO_FUNCTIONS \
60  OPT_SHOW_CLASS_HIERARCHY \
61  "(show-loops)" \
62  "(show-symbol-table)" \
63  "(list-symbols)" \
64  "(show-parse-tree)" \
65  OPT_SHOW_PROPERTIES \
66  "(drop-unused-functions)" \
67  "(property):(stop-on-fail)(trace)" \
68  "(verbosity):" \
69  "(nondet-static)" \
70  "(version)" \
71  "(symex-coverage-report):" \
72  OPT_TIMESTAMP \
73  "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)" \
74  "(ppc-macos)" \
75  "(arrays-uf-always)(arrays-uf-never)" \
76  "(no-arch)(arch):" \
77  OPT_FLUSH \
78  JAVA_BYTECODE_LANGUAGE_OPTIONS \
79  "(java-unwind-enum-static)" \
80  "(localize-faults)(localize-faults-method):" \
81  "(java-threading)" \
82  OPT_GOTO_TRACE \
83  "(symex-driven-lazy-loading)"
84 // clang-format on
85 
87  public parse_options_baset,
88  public messaget
89 {
90 public:
91  virtual int doit() override;
92  virtual void help() override;
93 
94  jbmc_parse_optionst(int argc, const char **argv);
96  int argc,
97  const char **argv,
98  const std::string &extra_options);
99 
104  static void set_default_options(optionst &);
105 
107  goto_model_functiont &function,
108  const abstract_goto_modelt &,
109  const optionst &);
110  bool process_goto_functions(goto_modelt &goto_model, const optionst &options);
111 
112  bool can_generate_function_body(const irep_idt &name);
113 
115  const irep_idt &function_name,
116  symbol_table_baset &symbol_table,
117  goto_functiont &function,
118  bool body_available);
119 
120 protected:
125 
126  std::unique_ptr<class_hierarchyt> class_hierarchy;
127 
129  int get_goto_program(
130  std::unique_ptr<goto_modelt> &goto_model, const optionst &);
131  bool show_loaded_functions(const abstract_goto_modelt &goto_model);
132 
133  bool set_properties(goto_modelt &goto_model);
134 };
135 
136 #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)
std::unique_ptr< class_hierarchyt > class_hierarchy
Abstract interface to eager or lazy GOTO models.
static void set_default_options(optionst &)
Set the options that have default values.
Traces of GOTO Programs.
void process_goto_function(goto_model_functiont &function, const abstract_goto_modelt &, const optionst &)
java_object_factory_parameterst object_factory_params
Factory and information for path_storaget.
Definition: path_storage.h:129
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)
Class Hierarchy.
bool can_generate_function_body(const irep_idt &name)
Abstract interface to support a programming language.
A collection of goto functions.
Program Transformation.
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
virtual int doit() override
invoke main modules
virtual void help() override
display command line help
A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers).
Definition: goto_function.h:26
String support via creating string constraints and progressively instantiating the universal constrai...
Author: Diffblue Ltd.
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 set_properties(goto_modelt &goto_model)
The symbol table base class interface.
Emit timestamps.
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
ui_message_handlert ui_message_handler
void get_command_line_options(optionst &)
Show the properties.
Storage of symbolic execution paths to resume.
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:153