cprover
goto_instrument_parse_options.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Command Line Parsing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
13 #define CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
14 
15 #include <util/ui_message.h>
16 #include <util/parse_options.h>
17 #include <util/timestamper.h>
18 
25 
26 #include <analyses/goto_check.h>
27 
29 
30 #include "count_eloc.h"
31 
32 // clang-format off
33 #define GOTO_INSTRUMENT_OPTIONS \
34  "(all)" \
35  "(document-claims-latex)(document-claims-html)" \
36  "(document-properties-latex)(document-properties-html)" \
37  "(dump-c)(dump-cpp)(no-system-headers)(use-all-headers)(dot)(xml)" \
38  "(harness)" \
39  OPT_GOTO_CHECK \
40  /* no-X-check are deprecated and ignored */ \
41  "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \
42  "(no-nan-check)" \
43  "(remove-pointers)" \
44  "(no-simplify)" \
45  "(assert-to-assume)" \
46  "(no-assertions)(no-assumptions)(uninitialized-check)" \
47  "(race-check)(scc)(one-event-per-cycle)" \
48  "(minimum-interference)" \
49  "(mm):(my-events)" \
50  "(unwind):(unwindset):(unwindset-file):" \
51  "(unwinding-assertions)(partial-loops)(continue-as-loops)" \
52  "(log):" \
53  "(max-var):(max-po-trans):(ignore-arrays)" \
54  "(cfg-kill)(no-dependencies)(force-loop-duplication)" \
55  "(call-graph)(reachable-call-graph)" \
56  OPT_SHOW_CLASS_HIERARCHY \
57  "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
58  "(nondet-volatile)(isr):" \
59  "(stack-depth):(nondet-static)" \
60  "(function-enter):(function-exit):(branch):" \
61  OPT_SHOW_GOTO_FUNCTIONS \
62  OPT_SHOW_PROPERTIES \
63  "(drop-unused-functions)" \
64  "(show-value-sets)" \
65  "(show-global-may-alias)" \
66  "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \
67  "(show-escape-analysis)(escape-analysis)" \
68  "(custom-bitvector-analysis)" \
69  "(show-struct-alignment)(interval-analysis)(show-intervals)" \
70  "(show-uninitialized)(show-locations)" \
71  "(full-slice)(reachability-slice)(slice-global-inits)" \
72  "(inline)(partial-inline)(function-inline):(log):(no-caching)" \
73  OPT_REMOVE_CONST_FUNCTION_POINTERS \
74  "(print-internal-representation)" \
75  "(remove-function-pointers)" \
76  "(show-claims)(property):" \
77  "(show-symbol-table)(show-points-to)(show-rw-set)" \
78  "(cav11)" \
79  OPT_TIMESTAMP \
80  "(show-natural-loops)(accelerate)(havoc-loops)" \
81  "(error-label):(string-abstraction)" \
82  "(verbosity):(version)(xml-ui)(json-ui)(show-loops)" \
83  "(accelerate)(constant-propagator)" \
84  "(k-induction):(step-case)(base-case)" \
85  "(show-call-sequences)(check-call-sequence)" \
86  "(interpreter)(show-reaching-definitions)" \
87  "(list-symbols)(list-undefined-functions)" \
88  "(z3)(add-library)(show-dependence-graph)" \
89  "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \
90  "(show-threaded)(list-calls-args)" \
91  "(undefined-function-is-assume-false)" \
92  "(remove-function-body):"\
93  OPT_FLUSH \
94  "(splice-call):" \
95  OPT_REMOVE_CALLS_NO_BODY \
96  OPT_REPLACE_FUNCTION_BODY \
97  OPT_GOTO_PROGRAM_STATS
98 
99 // clang-format on
100 
102  public parse_options_baset,
103  public messaget
104 {
105 public:
106  virtual int doit();
107  virtual void help();
108 
109  goto_instrument_parse_optionst(int argc, const char **argv):
112  ui_message_handler(cmdline, "goto-instrument"),
114  partial_inlining_done(false),
115  remove_returns_done(false)
116  {
117  }
118 
119 protected:
121  virtual void register_languages();
122 
123  void get_goto_program();
125 
126  void do_indirect_call_and_rtti_removal(bool force=false);
128  void do_partial_inlining();
129  void do_remove_returns();
130 
134 
136 
138  {
139  return ui_message_handler.get_ui();
140  }
141 };
142 
143 #endif // CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
void do_indirect_call_and_rtti_removal(bool force=false)
uit get_ui() const
Definition: ui_message.h:37
Show the goto functions.
Goto Programs with Functions.
Remove calls to functions without a body.
virtual int doit()
invoke main modules
Class Hierarchy.
goto_instrument_parse_optionst(int argc, const char **argv)
Program Transformation.
Count effective lines of code.
virtual void help()
display command line help
Emit timestamps.
Show the properties.
#define GOTO_INSTRUMENT_OPTIONS
void do_remove_const_function_pointers_only()
Remove function pointers that can be resolved by analysing const variables (i.e.