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>
16 
17 #include <util/parse_options.h>
18 #include <util/timestamper.h>
19 #include <util/ui_message.h>
21 
22 #include <langapi/language.h>
23 
24 #include <analyses/goto_check.h>
25 
26 #include <goto-checker/bmc_util.h>
27 
30 
32 
33 #include <json/json_interface.h>
34 #include <xmllang/xml_interface.h>
35 
36 #include <goto-instrument/cover.h>
37 
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  "(write-solver-stats-to):" \
50  "(show-array-constraints)" \
51  OPT_CONFIG_C_CPP \
52  OPT_CONFIG_PLATFORM \
53  OPT_CONFIG_BACKEND \
54  OPT_CONFIG_LIBRARY \
55  OPT_GOTO_CHECK \
56  OPT_XML_INTERFACE \
57  OPT_JSON_INTERFACE \
58  "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
59  "(cprover-smt2)" \
60  "(incremental-smt2-solver):" \
61  "(external-sat-solver):" \
62  "(no-sat-preprocessor)" \
63  "(beautify)" \
64  "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
65  OPT_STRING_REFINEMENT_CBMC \
66  OPT_SHOW_GOTO_FUNCTIONS \
67  OPT_SHOW_PROPERTIES \
68  "(show-symbol-table)(show-parse-tree)" \
69  "(drop-unused-functions)" \
70  "(havoc-undefined-functions)" \
71  "(property):(stop-on-fail)(trace)" \
72  "(verbosity):(no-library)" \
73  "(nondet-static)" \
74  "(version)" \
75  OPT_COVER \
76  "(symex-coverage-report):" \
77  "(mm):" \
78  OPT_TIMESTAMP \
79  "(arrays-uf-always)(arrays-uf-never)" \
80  OPT_FLUSH \
81  "(localize-faults)" \
82  OPT_GOTO_TRACE \
83  OPT_VALIDATE \
84  OPT_ANSI_C_LANGUAGE \
85  "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
86 // clang-format on
87 
89 {
90 public:
91  virtual int doit() override;
92  virtual void help() override;
93 
94  cbmc_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 
106  static bool process_goto_program(goto_modelt &, const optionst &, messaget &);
107 
108  static int get_goto_program(
109  goto_modelt &,
110  const optionst &,
111  const cmdlinet &,
113 
114 protected:
116 
117  void register_languages() override;
119  void preprocessing(const optionst &);
120  bool set_properties();
121 };
122 
123 #endif // CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
cbmc_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: cbmc_parse_options.cpp:509
cover.h
Coverage Instrumentation.
cbmc_parse_optionst::goto_model
goto_modelt goto_model
Definition: cbmc_parse_options.h:115
cbmc_parse_optionst::get_goto_program
static int get_goto_program(goto_modelt &, const optionst &, const cmdlinet &, ui_message_handlert &)
Definition: cbmc_parse_options.cpp:795
parse_options_baset
Definition: parse_options.h:20
ui_message_handlert
Definition: ui_message.h:22
optionst
Definition: options.h:23
json_interface.h
JSON Commandline Interface.
validation_interface.h
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition: goto_model.h:26
cbmc_parse_optionst::cbmc_parse_optionst
cbmc_parse_optionst(int argc, const char **argv)
Definition: cbmc_parse_options.cpp:79
goto_trace.h
Traces of GOTO Programs.
bmc_util.h
Bounded Model Checking Utilities.
cbmc_parse_optionst
Definition: cbmc_parse_options.h:89
cmdlinet
Definition: cmdline.h:21
cbmc_parse_optionst::get_command_line_options
void get_command_line_options(optionst &)
Definition: cbmc_parse_options.cpp:123
language.h
Abstract interface to support a programming language.
cbmc_parse_optionst::process_goto_program
static bool process_goto_program(goto_modelt &, const optionst &, messaget &)
Definition: cbmc_parse_options.cpp:879
string_refinement.h
String support via creating string constraints and progressively instantiating the universal constrai...
parse_options.h
goto_check.h
Program Transformation.
cbmc_parse_optionst::set_properties
bool set_properties()
Definition: cbmc_parse_options.cpp:784
ansi_c_language.h
cbmc_parse_optionst::help
virtual void help() override
display command line help
Definition: cbmc_parse_options.cpp:982
timestamper.h
Emit timestamps.
xml_interface.h
XML Interface.
cbmc_parse_optionst::register_languages
void register_languages() override
Definition: cbmc_languages.cpp:25
cbmc_parse_optionst::set_default_options
static void set_default_options(optionst &)
Set the options that have default values.
Definition: cbmc_parse_options.cpp:104
cbmc_parse_optionst::preprocessing
void preprocessing(const optionst &)
Definition: cbmc_parse_options.cpp:846
ui_message.h