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
19
#include <
goto-programs/class_hierarchy.h
>
20
#include <
goto-programs/goto_functions.h
>
21
#include <
goto-programs/remove_calls_no_body.h
>
22
#include <
goto-programs/remove_const_function_pointers.h
>
23
#include <
goto-programs/show_goto_functions.h
>
24
#include <
goto-programs/show_properties.h
>
25
26
#include <
analyses/goto_check.h
>
27
28
#include <
goto-programs/generate_function_bodies.h
>
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
101
class
goto_instrument_parse_optionst
:
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):
110
parse_options_baset
(
GOTO_INSTRUMENT_OPTIONS
, argc, argv),
111
messaget
(
ui_message_handler
),
112
ui_message_handler
(
cmdline
,
"goto-instrument"
),
113
function_pointer_removal_done
(false),
114
partial_inlining_done
(false),
115
remove_returns_done
(false)
116
{
117
}
118
119
protected
:
120
ui_message_handlert
ui_message_handler
;
121
virtual
void
register_languages
();
122
123
void
get_goto_program
();
124
void
instrument_goto_program
();
125
126
void
do_indirect_call_and_rtti_removal
(
bool
force=
false
);
127
void
do_remove_const_function_pointers_only
();
128
void
do_partial_inlining
();
129
void
do_remove_returns
();
130
131
bool
function_pointer_removal_done
;
132
bool
partial_inlining_done
;
133
bool
remove_returns_done
;
134
135
goto_modelt
goto_model
;
136
137
ui_message_handlert::uit
get_ui
()
138
{
139
return
ui_message_handler
.
get_ui
();
140
}
141
};
142
143
#endif // CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
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:803
goto_instrument_parse_optionst::goto_model
goto_modelt goto_model
Definition:
goto_instrument_parse_options.h:135
ui_message_handlert
Definition:
ui_message.h:19
ui_message_handlert::uit
uit
Definition:
ui_message.h:22
goto_instrument_parse_optionst::get_goto_program
void get_goto_program()
Definition:
goto_instrument_parse_options.cpp:867
ui_message_handlert::get_ui
uit get_ui() const
Definition:
ui_message.h:37
parse_options.h
goto_instrument_parse_optionst::remove_returns_done
bool remove_returns_done
Definition:
goto_instrument_parse_options.h:133
ui_message.h
show_goto_functions.h
Show the goto functions.
goto_functions.h
Goto Programs with Functions.
remove_calls_no_body.h
Remove calls to functions without a body.
goto_instrument_parse_optionst::ui_message_handler
ui_message_handlert ui_message_handler
Definition:
goto_instrument_parse_options.h:120
goto_instrument_parse_optionst::doit
virtual int doit()
invoke main modules
Definition:
goto_instrument_parse_options.cpp:103
goto_modelt
Definition:
goto_model.h:24
goto_instrument_parse_optionst::function_pointer_removal_done
bool function_pointer_removal_done
Definition:
goto_instrument_parse_options.h:131
class_hierarchy.h
Class Hierarchy.
goto_instrument_parse_optionst::do_remove_returns
void do_remove_returns()
Definition:
goto_instrument_parse_options.cpp:856
goto_instrument_parse_optionst::partial_inlining_done
bool partial_inlining_done
Definition:
goto_instrument_parse_options.h:132
generate_function_bodies.h
goto_instrument_parse_optionst::goto_instrument_parse_optionst
goto_instrument_parse_optionst(int argc, const char **argv)
Definition:
goto_instrument_parse_options.h:109
goto_check.h
Program Transformation.
messaget
Definition:
message.h:123
goto_instrument_parse_optionst::do_partial_inlining
void do_partial_inlining()
Definition:
goto_instrument_parse_options.cpp:842
count_eloc.h
Count effective lines of code.
goto_instrument_parse_optionst::instrument_goto_program
void instrument_goto_program()
Definition:
goto_instrument_parse_options.cpp:878
goto_instrument_parse_optionst::help
virtual void help()
display command line help
Definition:
goto_instrument_parse_options.cpp:1439
goto_instrument_parse_optionst
Definition:
goto_instrument_parse_options.h:101
timestamper.h
Emit timestamps.
goto_instrument_parse_optionst::get_ui
ui_message_handlert::uit get_ui()
Definition:
goto_instrument_parse_options.h:137
parse_options_baset::cmdline
cmdlinet cmdline
Definition:
parse_options.h:23
show_properties.h
Show the properties.
GOTO_INSTRUMENT_OPTIONS
#define GOTO_INSTRUMENT_OPTIONS
Definition:
goto_instrument_parse_options.h:33
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:825
parse_options_baset
Definition:
parse_options.h:17
goto_instrument_parse_optionst::register_languages
virtual void register_languages()
Definition:
goto_instrument_languages.cpp:19
remove_const_function_pointers.h
Goto Programs.
goto-instrument
goto_instrument_parse_options.h
Generated by
1.8.14