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
36 #define GOTO_INSTRUMENT_OPTIONS \
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)" \
44 "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \
48 "(assert-to-assume)" \
49 "(no-assertions)(no-assumptions)(uninitialized-check)" \
50 "(race-check)(scc)(one-event-per-cycle)" \
51 "(minimum-interference)" \
53 "(unwind):(unwindset):(unwindset-file):" \
54 "(unwinding-assertions)(partial-loops)(continue-as-loops)" \
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 \
66 "(drop-unused-functions)" \
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)" \
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 \
100 OPT_REMOVE_CALLS_NO_BODY \
101 OPT_REPLACE_FUNCTION_BODY \
102 OPT_GOTO_PROGRAM_STATS \
103 "(show-local-safe-pointers)(show-safe-dereferences)" \
105 "(validate-goto-binary)" \
153 #endif // CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
Class that provides messages with a built-in verbosity 'level'.
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()
virtual void register_languages()
bool partial_inlining_done
ui_message_handlert::uit get_ui()
ui_message_handlert ui_message_handler