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