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 <ansi-c/ansi_c_language.h>
17 
18 #include <util/parse_options.h>
19 #include <util/timestamper.h>
20 #include <util/ui_message.h>
22 
23 #include <langapi/language.h>
24 
25 #include <analyses/goto_check.h>
26 
28 
30 
32 
33 #include "bmc.h"
34 #include "xml_interface.h"
35 
36 class bmct;
37 class goto_functionst;
38 class optionst;
39 
40 // clang-format off
41 #define CBMC_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):(test-preprocessor)" \
49  "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
50  "(object-bits):" \
51  OPT_GOTO_CHECK \
52  "(no-assertions)(no-assumptions)" \
53  "(xml-ui)(xml-interface)(json-ui)" \
54  "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
55  "(cprover-smt2)" \
56  "(no-sat-preprocessor)" \
57  "(beautify)" \
58  "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
59  OPT_STRING_REFINEMENT_CBMC \
60  "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
61  "(little-endian)(big-endian)" \
62  OPT_SHOW_GOTO_FUNCTIONS \
63  OPT_SHOW_PROPERTIES \
64  "(show-symbol-table)(show-parse-tree)" \
65  "(drop-unused-functions)" \
66  "(property):(stop-on-fail)(trace)" \
67  "(error-label):(verbosity):(no-library)" \
68  "(nondet-static)" \
69  "(version)" \
70  "(cover):(symex-coverage-report):" \
71  "(mm):" \
72  OPT_TIMESTAMP \
73  "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
74  "(ppc-macos)(unsigned-char)" \
75  "(arrays-uf-always)(arrays-uf-never)" \
76  "(string-abstraction)(no-arch)(arch):" \
77  "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
78  OPT_FLUSH \
79  "(localize-faults)(localize-faults-method):" \
80  OPT_GOTO_TRACE \
81  OPT_VALIDATE \
82  OPT_ANSI_C_LANGUAGE \
83  "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
84 // clang-format on
85 
87  public parse_options_baset,
88  public xml_interfacet,
89  public messaget
90 {
91 public:
92  virtual int doit() override;
93  virtual void help() override;
94 
95  cbmc_parse_optionst(int argc, const char **argv);
97  int argc,
98  const char **argv,
99  const std::string &extra_options);
100 
105  static void set_default_options(optionst &);
106 
107  static bool process_goto_program(goto_modelt &, const optionst &, messaget &);
108 
109  static int get_goto_program(
110  goto_modelt &,
111  const optionst &,
112  const cmdlinet &,
113  messaget &,
115 
116 protected:
120 
121  void register_languages();
123  void preprocessing(const optionst &);
124  bool set_properties();
125 };
126 
127 #endif // CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
cbmc_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: cbmc_parse_options.cpp:418
cbmc_parse_optionst::goto_model
goto_modelt goto_model
Definition: cbmc_parse_options.h:117
parse_options_baset
Definition: parse_options.h:17
ui_message_handlert
Definition: ui_message.h:19
bmct
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
optionst
Definition: options.h:22
validation_interface.h
goto_modelt
Definition: goto_model.h:24
cbmc_parse_optionst::cbmc_parse_optionst
cbmc_parse_optionst(int argc, const char **argv)
Definition: cbmc_parse_options.cpp:66
xml_interfacet
Definition: xml_interface.h:19
cbmc_parse_optionst::register_languages
void register_languages()
Definition: cbmc_languages.cpp:24
goto_trace.h
cbmc_parse_optionst
Definition: cbmc_parse_options.h:86
cmdlinet
Definition: cmdline.h:19
c_object_factory_parameters.h
cbmc_parse_optionst::get_command_line_options
void get_command_line_options(optionst &)
Definition: cbmc_parse_options.cpp:103
cbmc_parse_optionst::get_goto_program
static int get_goto_program(goto_modelt &, const optionst &, const cmdlinet &, messaget &, ui_message_handlert &)
Definition: cbmc_parse_options.cpp:590
cbmc_parse_optionst::ui_message_handler
ui_message_handlert ui_message_handler
Definition: cbmc_parse_options.h:118
language.h
cbmc_parse_optionst::process_goto_program
static bool process_goto_program(goto_modelt &, const optionst &, messaget &)
Definition: cbmc_parse_options.cpp:730
string_refinement.h
parse_options.h
goto_check.h
solver_factory.h
cbmc_parse_optionst::set_properties
bool set_properties()
Definition: cbmc_parse_options.cpp:558
bmc.h
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
ansi_c_language.h
cbmc_parse_optionst::help
virtual void help() override
display command line help
Definition: cbmc_parse_options.cpp:892
timestamper.h
Emit timestamps.
path_strategy_choosert
Factory and information for path_storaget.
Definition: path_storage.h:129
xml_interface.h
cbmc_parse_optionst::path_strategy_chooser
const path_strategy_choosert path_strategy_chooser
Definition: cbmc_parse_options.h:119
cbmc_parse_optionst::set_default_options
static void set_default_options(optionst &)
Set the options that have default values.
Definition: cbmc_parse_options.cpp:87
cbmc_parse_optionst::preprocessing
void preprocessing(const optionst &)
Definition: cbmc_parse_options.cpp:673
ui_message.h