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 
26 
27 #include <analyses/goto_check.h>
28 
30 #include "aggressive_slicer.h"
31 
32 #include "count_eloc.h"
33 
34 // clang-format off
35 #define GOTO_INSTRUMENT_OPTIONS \
36  "(all)" \
37  "(document-claims-latex)(document-claims-html)" \
38  "(document-properties-latex)(document-properties-html)" \
39  "(dump-c)(dump-cpp)(no-system-headers)(use-all-headers)(dot)(xml)" \
40  "(harness)" \
41  OPT_GOTO_CHECK \
42  /* no-X-check are deprecated and ignored */ \
43  "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \
44  "(no-nan-check)" \
45  "(remove-pointers)" \
46  "(no-simplify)" \
47  "(assert-to-assume)" \
48  "(no-assertions)(no-assumptions)(uninitialized-check)" \
49  "(race-check)(scc)(one-event-per-cycle)" \
50  "(minimum-interference)" \
51  "(mm):(my-events)" \
52  "(unwind):(unwindset):(unwindset-file):" \
53  "(unwinding-assertions)(partial-loops)(continue-as-loops)" \
54  "(log):" \
55  "(max-var):(max-po-trans):(ignore-arrays)" \
56  "(cfg-kill)(no-dependencies)(force-loop-duplication)" \
57  "(call-graph)(reachable-call-graph)" \
58  OPT_SHOW_CLASS_HIERARCHY \
59  "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
60  "(nondet-volatile)(isr):" \
61  "(stack-depth):(nondet-static)" \
62  "(function-enter):(function-exit):(branch):" \
63  OPT_SHOW_GOTO_FUNCTIONS \
64  OPT_SHOW_PROPERTIES \
65  "(drop-unused-functions)" \
66  "(show-value-sets)" \
67  "(show-global-may-alias)" \
68  "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \
69  "(show-escape-analysis)(escape-analysis)" \
70  "(custom-bitvector-analysis)" \
71  "(show-struct-alignment)(interval-analysis)(show-intervals)" \
72  "(show-uninitialized)(show-locations)" \
73  "(full-slice)(reachability-slice)(slice-global-inits)" \
74  "(inline)(partial-inline)(function-inline):(log):(no-caching)" \
75  OPT_REMOVE_CONST_FUNCTION_POINTERS \
76  "(print-internal-representation)" \
77  "(remove-function-pointers)" \
78  "(show-claims)(property):" \
79  "(show-symbol-table)(show-points-to)(show-rw-set)" \
80  "(cav11)" \
81  OPT_TIMESTAMP \
82  "(show-natural-loops)(accelerate)(havoc-loops)" \
83  "(error-label):(string-abstraction)" \
84  "(verbosity):(version)(xml-ui)(json-ui)(show-loops)" \
85  "(accelerate)(constant-propagator)" \
86  "(k-induction):(step-case)(base-case)" \
87  "(show-call-sequences)(check-call-sequence)" \
88  "(interpreter)(show-reaching-definitions)" \
89  "(list-symbols)(list-undefined-functions)" \
90  "(z3)(add-library)(show-dependence-graph)" \
91  "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \
92  "(show-threaded)(list-calls-args)" \
93  "(undefined-function-is-assume-false)" \
94  "(remove-function-body):"\
95  OPT_AGGRESSIVE_SLICER \
96  OPT_FLUSH \
97  "(splice-call):" \
98  OPT_REMOVE_CALLS_NO_BODY \
99  OPT_REPLACE_FUNCTION_BODY \
100  OPT_GOTO_PROGRAM_STATS \
101  "(show-local-safe-pointers)(show-safe-dereferences)" \
102  OPT_REPLACE_CALLS \
103  // empty last line
104 
105 // clang-format on
106 
108  public parse_options_baset,
109  public messaget
110 {
111 public:
112  virtual int doit();
113  virtual void help();
114 
115  goto_instrument_parse_optionst(int argc, const char **argv):
118  ui_message_handler(cmdline, "goto-instrument"),
120  partial_inlining_done(false),
121  remove_returns_done(false)
122  {
123  }
124 
125 protected:
127  virtual void register_languages();
128 
129  void get_goto_program();
131 
132  void do_indirect_call_and_rtti_removal(bool force=false);
134  void do_partial_inlining();
135  void do_remove_returns();
136 
140 
142 
144  {
145  return ui_message_handler.get_ui();
146  }
147 };
148 
149 #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.
Replace calls to given functions with calls to other given functions.
virtual void help()
display command line help
Emit timestamps.
Aggressive slicer Consider the control flow graph of the goto program and a criterion description of ...
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.