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/config.h>
19 #include <util/parse_options.h>
20 #include <util/timestamper.h>
21 #include <util/ui_message.h>
23 
24 #include <langapi/language.h>
25 
26 #include <analyses/goto_check.h>
27 
28 #include <goto-checker/bmc_util.h>
30 
32 
34 
35 #include <json/json_interface.h>
36 #include <xmllang/xml_interface.h>
37 
38 #include <goto-instrument/cover.h>
39 
40 class goto_functionst;
41 class optionst;
42 
43 // clang-format off
44 #define CBMC_OPTIONS \
45  OPT_BMC \
46  "(preprocess)(slice-by-trace):" \
47  OPT_FUNCTIONS \
48  "(no-simplify)(full-slice)" \
49  OPT_REACHABILITY_SLICER \
50  "(debug-level):(no-propagation)(no-simplify-if)" \
51  "(document-subgoals)(outfile):(test-preprocessor)" \
52  "(write-solver-stats-to):" \
53  "(show-array-constraints)" \
54  OPT_CONFIG_C_CPP \
55  OPT_CONFIG_PLATFORM \
56  OPT_CONFIG_BACKEND \
57  OPT_CONFIG_LIBRARY \
58  OPT_GOTO_CHECK \
59  OPT_XML_INTERFACE \
60  OPT_JSON_INTERFACE \
61  "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
62  "(cprover-smt2)" \
63  "(external-sat-solver):" \
64  "(no-sat-preprocessor)" \
65  "(beautify)" \
66  "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
67  OPT_STRING_REFINEMENT_CBMC \
68  OPT_SHOW_GOTO_FUNCTIONS \
69  OPT_SHOW_PROPERTIES \
70  "(show-symbol-table)(show-parse-tree)" \
71  "(drop-unused-functions)" \
72  "(havoc-undefined-functions)" \
73  "(property):(stop-on-fail)(trace)" \
74  "(verbosity):(no-library)" \
75  "(nondet-static)" \
76  "(version)" \
77  OPT_COVER \
78  "(symex-coverage-report):" \
79  "(mm):" \
80  OPT_TIMESTAMP \
81  "(arrays-uf-always)(arrays-uf-never)" \
82  OPT_FLUSH \
83  "(localize-faults)" \
84  OPT_GOTO_TRACE \
85  OPT_VALIDATE \
86  OPT_ANSI_C_LANGUAGE \
87  "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
88 // clang-format on
89 
91 {
92 public:
93  virtual int doit() override;
94  virtual void help() override;
95 
96  cbmc_parse_optionst(int argc, const char **argv);
98  int argc,
99  const char **argv,
100  const std::string &extra_options);
101 
106  static void set_default_options(optionst &);
107 
108  static bool process_goto_program(goto_modelt &, const optionst &, messaget &);
109 
110  static int get_goto_program(
111  goto_modelt &,
112  const optionst &,
113  const cmdlinet &,
115 
116 protected:
118 
119  void register_languages();
121  void preprocessing(const optionst &);
122  bool set_properties();
123 };
124 
125 #endif // CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
Bounded Model Checking Utilities.
virtual int doit() override
invoke main modules
static bool process_goto_program(goto_modelt &, const optionst &, messaget &)
static void set_default_options(optionst &)
Set the options that have default values.
static int get_goto_program(goto_modelt &, const optionst &, const cmdlinet &, ui_message_handlert &)
void get_command_line_options(optionst &)
void preprocessing(const optionst &)
virtual void help() override
display command line help
cbmc_parse_optionst(int argc, const char **argv)
A collection of goto functions.
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
Coverage Instrumentation.
Program Transformation.
Traces of GOTO Programs.
JSON Commandline Interface.
Abstract interface to support a programming language.
Solver Factory.
String support via creating string constraints and progressively instantiating the universal constrai...
Emit timestamps.
XML Interface.