12 #ifndef CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H 13 #define CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H 25 #define GOTO_INSTRUMENT_OPTIONS \ 27 "(document-claims-latex)(document-claims-html)" \ 28 "(document-properties-latex)(document-properties-html)" \ 29 "(dump-c)(dump-cpp)(no-system-headers)(use-all-headers)(dot)(xml)" \ 32 "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \ 36 "(assert-to-assume)" \ 37 "(no-assertions)(no-assumptions)(uninitialized-check)" \ 38 "(race-check)(scc)(one-event-per-cycle)" \ 39 "(minimum-interference)" \ 41 "(unwind):(unwindset):(unwindset-file):" \ 42 "(unwinding-assertions)(partial-loops)(continue-as-loops)" \ 44 "(max-var):(max-po-trans):(ignore-arrays)" \ 45 "(cfg-kill)(no-dependencies)(force-loop-duplication)" \ 47 "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \ 48 "(nondet-volatile)(isr):" \ 49 "(stack-depth):(nondet-static)" \ 50 "(function-enter):(function-exit):(branch):" \ 51 OPT_SHOW_GOTO_FUNCTIONS \ 52 "(drop-unused-functions)" \ 54 "(show-global-may-alias)" \ 55 "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \ 56 "(show-escape-analysis)(escape-analysis)" \ 57 "(custom-bitvector-analysis)" \ 58 "(show-struct-alignment)(interval-analysis)(show-intervals)" \ 59 "(show-uninitialized)(show-locations)" \ 60 "(full-slice)(reachability-slice)(slice-global-inits)" \ 61 "(inline)(partial-inline)(function-inline):(log):(no-caching)" \ 62 OPT_REMOVE_CONST_FUNCTION_POINTERS \ 63 "(print-internal-representation)" \ 64 "(remove-function-pointers)" \ 65 "(show-claims)(show-properties)(property):" \ 66 "(show-symbol-table)(show-points-to)(show-rw-set)" \ 68 "(show-natural-loops)(accelerate)(havoc-loops)" \ 69 "(error-label):(string-abstraction)" \ 70 "(verbosity):(version)(xml-ui)(json-ui)(show-loops)" \ 71 "(accelerate)(constant-propagator)" \ 72 "(k-induction):(step-case)(base-case)" \ 73 "(show-call-sequences)(check-call-sequence)" \ 74 "(interpreter)(show-reaching-definitions)(count-eloc)(list-eloc)" \ 75 "(list-symbols)(list-undefined-functions)" \ 76 "(z3)(add-library)(show-dependence-graph)" \ 77 "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \ 78 "(show-threaded)(list-calls-args)(print-path-lengths)" \ 79 "(undefined-function-is-assume-false)" \ 80 "(remove-function-body):" 121 #endif // CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H void do_indirect_call_and_rtti_removal(bool force=false)
Goto Programs with Functions.
ui_message_handlert ui_message_handler
virtual int doit()
invoke main modules
bool function_pointer_removal_done
bool partial_inlining_done
goto_instrument_parse_optionst(int argc, const char **argv)
void do_partial_inlining()
void instrument_goto_program()
virtual void help()
display command line help
#define GOTO_INSTRUMENT_OPTIONS
void do_remove_const_function_pointers_only()
Remove function pointers that can be resolved by analysing const variables (i.e.
goto_functionst goto_functions
virtual void register_languages()