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