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 <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 
29 
30 #include <analyses/goto_check.h>
31 
32 #include "aggressive_slicer.h"
33 #include "code_contracts.h"
36 #include "nondet_volatile.h"
37 #include "replace_calls.h"
38 
39 #include "count_eloc.h"
40 
41 // clang-format off
42 #define GOTO_INSTRUMENT_OPTIONS \
43  "(all)" \
44  "(document-claims-latex)(document-claims-html)" \
45  "(document-properties-latex)(document-properties-html)" \
46  "(dump-c-type-header):" \
47  "(dump-c)(dump-cpp)(no-system-headers)(use-all-headers)(dot)(xml)" \
48  "(harness)" \
49  OPT_GOTO_CHECK \
50  /* no-X-check are deprecated and ignored */ \
51  "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \
52  "(no-nan-check)" \
53  "(remove-pointers)" \
54  "(no-simplify)" \
55  "(assert-to-assume)" \
56  "(no-assertions)(no-assumptions)(uninitialized-check)" \
57  "(race-check)(scc)(one-event-per-cycle)" \
58  "(minimum-interference)" \
59  "(mm):(my-events)" \
60  "(unwind):(unwindset):(unwindset-file):" \
61  "(unwinding-assertions)(partial-loops)(continue-as-loops)" \
62  "(log):" \
63  "(max-var):(max-po-trans):(ignore-arrays)" \
64  "(cfg-kill)(no-dependencies)(force-loop-duplication)" \
65  "(call-graph)(reachable-call-graph)" \
66  OPT_INSERT_FINAL_ASSERT_FALSE \
67  OPT_SHOW_CLASS_HIERARCHY \
68  "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
69  "(isr):" \
70  "(stack-depth):(nondet-static)" \
71  "(nondet-static-exclude):" \
72  "(function-enter):(function-exit):(branch):" \
73  OPT_SHOW_GOTO_FUNCTIONS \
74  OPT_SHOW_PROPERTIES \
75  "(drop-unused-functions)" \
76  "(show-value-sets)" \
77  "(show-global-may-alias)" \
78  "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \
79  "(show-escape-analysis)(escape-analysis)" \
80  "(custom-bitvector-analysis)" \
81  "(show-struct-alignment)(interval-analysis)(show-intervals)" \
82  "(show-uninitialized)(show-locations)" \
83  "(full-slice)(reachability-slice)(slice-global-inits)" \
84  "(fp-reachability-slice):" \
85  "(inline)(partial-inline)(function-inline):(log):(no-caching)" \
86  "(value-set-fi-fp-removal)" \
87  OPT_REMOVE_CONST_FUNCTION_POINTERS \
88  "(print-internal-representation)" \
89  "(remove-function-pointers)" \
90  "(show-claims)(property):" \
91  "(show-symbol-table)(show-points-to)(show-rw-set)" \
92  "(cav11)" \
93  OPT_TIMESTAMP \
94  "(show-natural-loops)(show-lexical-loops)(accelerate)(havoc-loops)" \
95  "(error-label):(string-abstraction)" \
96  "(verbosity):(version)(xml-ui)(json-ui)(show-loops)" \
97  "(accelerate)(constant-propagator)" \
98  "(k-induction):(step-case)(base-case)" \
99  "(show-call-sequences)(check-call-sequence)" \
100  "(interpreter)(show-reaching-definitions)" \
101  "(list-symbols)(list-undefined-functions)" \
102  "(z3)(add-library)(show-dependence-graph)" \
103  "(horn)(skip-loops):(model-argc-argv):" \
104  "(" FLAG_REPLACE_CALL "):" \
105  "(" FLAG_REPLACE_ALL_CALLS ")" \
106  "(" FLAG_ENFORCE_CONTRACT "):" \
107  "(" FLAG_ENFORCE_ALL_CONTRACTS ")" \
108  "(show-threaded)(list-calls-args)" \
109  "(undefined-function-is-assume-false)" \
110  "(remove-function-body):"\
111  OPT_AGGRESSIVE_SLICER \
112  OPT_FLUSH \
113  "(splice-call):" \
114  OPT_REMOVE_CALLS_NO_BODY \
115  OPT_REPLACE_FUNCTION_BODY \
116  OPT_GOTO_PROGRAM_STATS \
117  "(show-local-safe-pointers)(show-safe-dereferences)" \
118  "(show-sese-regions)" \
119  OPT_REPLACE_CALLS \
120  "(validate-goto-binary)" \
121  OPT_VALIDATE \
122  OPT_ANSI_C_LANGUAGE \
123  OPT_RESTRICT_FUNCTION_POINTER \
124  OPT_NONDET_VOLATILE \
125  "(ensure-one-backedge-per-target)" \
126  // empty last line
127 
128 // clang-format on
129 
131 {
132 public:
133  virtual int doit();
134  virtual void help();
135 
136  goto_instrument_parse_optionst(int argc, const char **argv)
139  argc,
140  argv,
141  "goto-instrument"),
143  partial_inlining_done(false),
144  remove_returns_done(false)
145  {
146  }
147 
148 protected:
149  void register_languages();
150 
151  void get_goto_program();
153 
154  void do_indirect_call_and_rtti_removal(bool force=false);
156  void do_partial_inlining();
157  void do_remove_returns();
158 
162 
164 };
165 
166 #endif // CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
goto_instrument_parse_optionst
Definition: goto_instrument_parse_options.h:131
parse_options_baset
Definition: parse_options.h:20
goto_instrument_parse_optionst::do_remove_returns
void do_remove_returns()
Definition: goto_instrument_parse_options.cpp:969
goto_instrument_parse_optionst::help
virtual void help()
display command line help
Definition: goto_instrument_parse_options.cpp:1749
goto_instrument_parse_optionst::do_partial_inlining
void do_partial_inlining()
Definition: goto_instrument_parse_options.cpp:955
goto_instrument_parse_optionst::goto_instrument_parse_optionst
goto_instrument_parse_optionst(int argc, const char **argv)
Definition: goto_instrument_parse_options.h:136
goto_instrument_parse_optionst::function_pointer_removal_done
bool function_pointer_removal_done
Definition: goto_instrument_parse_options.h:159
validation_interface.h
count_eloc.h
Count effective lines of code.
remove_calls_no_body.h
Remove calls to functions without a body.
goto_instrument_parse_optionst::do_remove_const_function_pointers_only
void do_remove_const_function_pointers_only()
Remove function pointers that can be resolved by analysing const variables (i.e.
Definition: goto_instrument_parse_options.cpp:938
goto_modelt
Definition: goto_model.h:26
show_goto_functions.h
Show the goto functions.
insert_final_assert_false.h
Insert final assert false into a function.
replace_calls.h
Replace calls to given functions with calls to other given functions.
generate_function_bodies.h
goto_instrument_parse_optionst::doit
virtual int doit()
invoke main modules
Definition: goto_instrument_parse_options.cpp:119
GOTO_INSTRUMENT_OPTIONS
#define GOTO_INSTRUMENT_OPTIONS
Definition: goto_instrument_parse_options.h:42
goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal
void do_indirect_call_and_rtti_removal(bool force=false)
Definition: goto_instrument_parse_options.cpp:918
restrict_function_pointers.h
Given goto functions and a list of function parameters or globals that are function pointers with lis...
goto_instrument_parse_optionst::get_goto_program
void get_goto_program()
Definition: goto_instrument_parse_options.cpp:980
show_properties.h
Show the properties.
goto_instrument_parse_optionst::instrument_goto_program
void instrument_goto_program()
Definition: goto_instrument_parse_options.cpp:997
parse_options.h
goto_check.h
Program Transformation.
goto_instrument_parse_optionst::register_languages
void register_languages()
Definition: goto_instrument_languages.cpp:19
goto_instrument_parse_optionst::partial_inlining_done
bool partial_inlining_done
Definition: goto_instrument_parse_options.h:160
aggressive_slicer.h
Aggressive slicer Consider the control flow graph of the goto program and a criterion description of ...
goto_instrument_parse_optionst::remove_returns_done
bool remove_returns_done
Definition: goto_instrument_parse_options.h:161
class_hierarchy.h
Class Hierarchy.
remove_const_function_pointers.h
Goto Programs.
ansi_c_language.h
nondet_volatile.h
Volatile Variables.
goto_functions.h
Goto Programs with Functions.
timestamper.h
Emit timestamps.
goto_instrument_parse_optionst::goto_model
goto_modelt goto_model
Definition: goto_instrument_parse_options.h:163
code_contracts.h
Verify and use annotated invariants and pre/post-conditions.
ui_message.h