cprover
cbmc_parse_options.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: CBMC Command Line Option Processing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
13 #define CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
14 
15 #include <util/ui_message.h>
16 #include <util/parse_options.h>
17 
18 #include <langapi/language_ui.h>
19 
20 #include <analyses/goto_check.h>
21 
22 #include "xml_interface.h"
23 
24 class bmct;
25 class goto_functionst;
26 class optionst;
27 
28 #define CBMC_OPTIONS \
29  "(program-only)(function):(preprocess)(slice-by-trace):" \
30  "(no-simplify)(unwind):(unwindset):(slice-formula)(full-slice)" \
31  "(debug-level):(no-propagation)(no-simplify-if)" \
32  "(document-subgoals)(outfile):(test-preprocessor)" \
33  "D:I:(c89)(c99)(c11)(cpp89)(cpp99)(cpp11)" \
34  "(classpath):(cp):(main-class):" \
35  "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \
36  OPT_GOTO_CHECK \
37  "(no-assertions)(no-assumptions)" \
38  "(no-built-in-assertions)" \
39  "(xml-ui)(xml-interface)(json-ui)" \
40  "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \
41  "(no-sat-preprocessor)" \
42  "(no-pretty-names)(beautify)" \
43  "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
44  "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
45  "(little-endian)(big-endian)" \
46  "(show-goto-functions)(show-loops)" \
47  "(show-symbol-table)(show-parse-tree)(show-vcc)" \
48  "(show-claims)(claim):(show-properties)" \
49  "(drop-unused-functions)" \
50  "(property):(stop-on-fail)(trace)" \
51  "(error-label):(verbosity):(no-library)" \
52  "(nondet-static)" \
53  "(version)" \
54  "(cover):(symex-coverage-report):" \
55  "(mm):" \
56  "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
57  "(ppc-macos)(unsigned-char)" \
58  "(arrays-uf-always)(arrays-uf-never)" \
59  "(string-abstraction)(no-arch)(arch):" \
60  "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
61  "(graphml-witness):" \
62  "(java-max-vla-length):(java-unwind-enum-static)" \
63  "(java-cp-include-files):" \
64  "(localize-faults)(localize-faults-method):" \
65  "(lazy-methods)" \
66  "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
67 
69  public parse_options_baset,
70  public xml_interfacet,
71  public language_uit
72 {
73 public:
74  virtual int doit() override;
75  virtual void help() override;
76 
77  cbmc_parse_optionst(int argc, const char **argv);
79  int argc,
80  const char **argv,
81  const std::string &extra_options);
82 
83 protected:
85  virtual void register_languages();
86 
87  virtual void get_command_line_options(optionst &options);
88 
89  virtual int do_bmc(
90  bmct &bmc,
91  const goto_functionst &goto_functions);
92 
93  virtual int get_goto_program(
94  const optionst &options,
95  expr_listt &bmc_constraints,
96  goto_functionst &goto_functions);
97 
98  virtual bool process_goto_program(
99  const optionst &options,
100  goto_functionst &goto_functions);
101 
102  bool set_properties(goto_functionst &goto_functions);
103 
104  void eval_verbosity();
105 
106  // get any additional stuff before finalizing the goto program
107  virtual int get_modules(expr_listt &bmc_constraints)
108  {
109  return -1; // continue
110  }
111 
112  void preprocessing();
113 };
114 
115 #endif // CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
bool set_properties(goto_functionst &goto_functions)
virtual void get_command_line_options(optionst &options)
virtual int do_bmc(bmct &bmc, const goto_functionst &goto_functions)
invoke main modules
virtual bool process_goto_program(const optionst &options, goto_functionst &goto_functions)
virtual int get_modules(expr_listt &bmc_constraints)
Program Transformation.
std::list< exprt > expr_listt
Definition: expr.h:166
virtual int doit() override
invoke main modules
virtual int get_goto_program(const optionst &options, expr_listt &bmc_constraints, goto_functionst &goto_functions)
cbmc_parse_optionst(int argc, const char **argv)
Definition: bmc.h:32
ui_message_handlert ui_message_handler
XML Interface.
virtual void help() override
display command line help
virtual void register_languages()