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 #include <util/timestamper.h>
18 
19 #include <langapi/language.h>
20 
21 #include <analyses/goto_check.h>
22 
24 
25 #include "bmc.h"
26 #include "xml_interface.h"
27 #include "cbmc_solvers.h"
28 
29 class bmct;
30 class goto_functionst;
31 class optionst;
32 
33 // clang-format off
34 #define CBMC_OPTIONS \
35  OPT_BMC \
36  "(preprocess)(slice-by-trace):" \
37  OPT_FUNCTIONS \
38  "(no-simplify)(full-slice)" \
39  OPT_REACHABILITY_SLICER \
40  "(debug-level):(no-propagation)(no-simplify-if)" \
41  "(document-subgoals)(outfile):(test-preprocessor)" \
42  "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
43  "(object-bits):" \
44  OPT_GOTO_CHECK \
45  "(no-assertions)(no-assumptions)" \
46  "(no-built-in-assertions)" \
47  "(xml-ui)(xml-interface)(json-ui)" \
48  "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \
49  "(no-sat-preprocessor)" \
50  "(beautify)" \
51  "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
52  "(refine-strings)" \
53  "(string-printable)" \
54  "(string-max-length):" \
55  "(string-max-input-length):" \
56  "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
57  "(little-endian)(big-endian)" \
58  OPT_SHOW_GOTO_FUNCTIONS \
59  OPT_SHOW_PROPERTIES \
60  "(show-symbol-table)(show-parse-tree)" \
61  "(drop-unused-functions)" \
62  "(property):(stop-on-fail)(trace)" \
63  "(error-label):(verbosity):(no-library)" \
64  "(nondet-static)" \
65  "(version)" \
66  "(cover):(symex-coverage-report):" \
67  "(mm):" \
68  OPT_TIMESTAMP \
69  "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
70  "(ppc-macos)(unsigned-char)" \
71  "(arrays-uf-always)(arrays-uf-never)" \
72  "(string-abstraction)(no-arch)(arch):" \
73  "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
74  OPT_FLUSH \
75  "(localize-faults)(localize-faults-method):" \
76  OPT_GOTO_TRACE \
77  "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
78 // clang-format on
79 
81  public parse_options_baset,
82  public xml_interfacet,
83  public messaget
84 {
85 public:
86  virtual int doit() override;
87  virtual void help() override;
88 
89  cbmc_parse_optionst(int argc, const char **argv);
91  int argc,
92  const char **argv,
93  const std::string &extra_options);
94 
99  static void set_default_options(optionst &);
100 
101  static bool process_goto_program(goto_modelt &, const optionst &, messaget &);
102 
103  static int get_goto_program(
104  goto_modelt &,
105  const optionst &,
106  const cmdlinet &,
107  messaget &,
109 
110 protected:
114 
115  void register_languages();
117  void preprocessing();
118  bool set_properties();
119 };
120 
121 #endif // CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
void get_command_line_options(optionst &)
static int get_goto_program(goto_modelt &, const optionst &, const cmdlinet &, messaget &, ui_message_handlert &)
Traces of GOTO Programs.
const path_strategy_choosert path_strategy_chooser
Factory and information for path_storaget.
Definition: path_storage.h:119
static bool process_goto_program(goto_modelt &, const optionst &, messaget &)
Abstract interface to support a programming language.
Program Transformation.
virtual int doit() override
invoke main modules
static void set_default_options(optionst &)
Set the options that have default values.
Bounded Model Checking for ANSI-C + HDL.
cbmc_parse_optionst(int argc, const char **argv)
Emit timestamps.
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
Bounded Model Checking for ANSI-C + HDL.
ui_message_handlert ui_message_handler
XML Interface.
virtual void help() override
display command line help