Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
13 #define CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
39 #define GOTO_INSTRUMENT_OPTIONS \
41 "(document-claims-latex)(document-claims-html)" \
42 "(document-properties-latex)(document-properties-html)" \
43 "(dump-c-type-header):" \
44 "(dump-c)(dump-cpp)(no-system-headers)(use-all-headers)(dot)(xml)" \
48 "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \
52 "(assert-to-assume)" \
53 "(no-assertions)(no-assumptions)(uninitialized-check)" \
54 "(race-check)(scc)(one-event-per-cycle)" \
55 "(minimum-interference)" \
57 "(unwind):(unwindset):(unwindset-file):" \
58 "(unwinding-assertions)(partial-loops)(continue-as-loops)" \
60 "(max-var):(max-po-trans):(ignore-arrays)" \
61 "(cfg-kill)(no-dependencies)(force-loop-duplication)" \
62 "(call-graph)(reachable-call-graph)" \
63 OPT_INSERT_FINAL_ASSERT_FALSE \
64 OPT_SHOW_CLASS_HIERARCHY \
65 "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
66 "(nondet-volatile)(isr):" \
67 "(stack-depth):(nondet-static)" \
68 "(nondet-static-exclude):" \
69 "(function-enter):(function-exit):(branch):" \
70 OPT_SHOW_GOTO_FUNCTIONS \
72 "(drop-unused-functions)" \
74 "(show-global-may-alias)" \
75 "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \
76 "(show-escape-analysis)(escape-analysis)" \
77 "(custom-bitvector-analysis)" \
78 "(show-struct-alignment)(interval-analysis)(show-intervals)" \
79 "(show-uninitialized)(show-locations)" \
80 "(full-slice)(reachability-slice)(slice-global-inits)" \
81 "(fp-reachability-slice):" \
82 "(inline)(partial-inline)(function-inline):(log):(no-caching)" \
83 OPT_REMOVE_CONST_FUNCTION_POINTERS \
84 "(print-internal-representation)" \
85 "(remove-function-pointers)" \
86 "(show-claims)(property):" \
87 "(show-symbol-table)(show-points-to)(show-rw-set)" \
90 "(show-natural-loops)(show-lexical-loops)(accelerate)(havoc-loops)" \
91 "(error-label):(string-abstraction)" \
92 "(verbosity):(version)(xml-ui)(json-ui)(show-loops)" \
93 "(accelerate)(constant-propagator)" \
94 "(k-induction):(step-case)(base-case)" \
95 "(show-call-sequences)(check-call-sequence)" \
96 "(interpreter)(show-reaching-definitions)" \
97 "(list-symbols)(list-undefined-functions)" \
98 "(z3)(add-library)(show-dependence-graph)" \
99 "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \
100 "(show-threaded)(list-calls-args)" \
101 "(undefined-function-is-assume-false)" \
102 "(remove-function-body):"\
103 OPT_AGGRESSIVE_SLICER \
106 OPT_REMOVE_CALLS_NO_BODY \
107 OPT_REPLACE_FUNCTION_BODY \
108 OPT_GOTO_PROGRAM_STATS \
109 "(show-local-safe-pointers)(show-safe-dereferences)" \
110 "(show-sese-regions)" \
112 "(validate-goto-binary)" \
114 OPT_ANSI_C_LANGUAGE \
115 "(ensure-one-backedge-per-target)" \
156 #endif // CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
virtual void help()
display command line help
void do_partial_inlining()
goto_instrument_parse_optionst(int argc, const char **argv)
bool function_pointer_removal_done
void do_remove_const_function_pointers_only()
Remove function pointers that can be resolved by analysing const variables (i.e.
virtual int doit()
invoke main modules
#define GOTO_INSTRUMENT_OPTIONS
void do_indirect_call_and_rtti_removal(bool force=false)
void instrument_goto_program()
void register_languages()
bool partial_inlining_done