12 #ifndef CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
13 #define CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
42 #define GOTO_INSTRUMENT_OPTIONS \
44 "(document-claims-latex)(document-claims-html)" \
45 "(document-properties-latex)(document-properties-html)" \
46 "(dump-c-type-header):" \
47 "(dump-c)(dump-cpp)(no-system-headers)(use-all-headers)(dot)(xml)" \
51 "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \
55 "(uninitialized-check)" \
56 "(race-check)(scc)(one-event-per-cycle)" \
57 "(minimum-interference)" \
59 "(unwind):(unwindset):(unwindset-file):" \
60 "(unwinding-assertions)(partial-loops)(continue-as-loops)" \
62 "(max-var):(max-po-trans):(ignore-arrays)" \
63 "(cfg-kill)(no-dependencies)(force-loop-duplication)" \
64 "(call-graph)(reachable-call-graph)" \
65 OPT_INSERT_FINAL_ASSERT_FALSE \
66 OPT_SHOW_CLASS_HIERARCHY \
67 "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
69 "(stack-depth):(nondet-static)" \
70 "(nondet-static-exclude):" \
71 "(function-enter):(function-exit):(branch):" \
72 OPT_SHOW_GOTO_FUNCTIONS \
74 "(drop-unused-functions)" \
76 "(show-global-may-alias)" \
77 "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \
78 "(show-escape-analysis)(escape-analysis)" \
79 "(custom-bitvector-analysis)" \
80 "(show-struct-alignment)(interval-analysis)(show-intervals)" \
81 "(show-uninitialized)(show-locations)" \
82 "(full-slice)(reachability-slice)(slice-global-inits)" \
83 "(fp-reachability-slice):" \
84 "(inline)(partial-inline)(function-inline):(log):(no-caching)" \
85 "(value-set-fi-fp-removal)" \
86 OPT_REMOVE_CONST_FUNCTION_POINTERS \
87 "(print-internal-representation)" \
88 "(remove-function-pointers)" \
89 "(show-claims)(property):" \
90 "(show-symbol-table)(show-points-to)(show-rw-set)" \
93 "(show-natural-loops)(show-lexical-loops)(accelerate)(havoc-loops)" \
94 "(string-abstraction)" \
95 "(verbosity):(version)(xml-ui)(json-ui)(show-loops)" \
96 "(accelerate)(constant-propagator)" \
97 "(k-induction):(step-case)(base-case)" \
98 "(show-call-sequences)(check-call-sequence)" \
99 "(interpreter)(show-reaching-definitions)" \
100 "(list-symbols)(list-undefined-functions)" \
101 "(z3)(add-library)(show-dependence-graph)" \
102 "(horn)(skip-loops):(model-argc-argv):" \
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 \
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)" \
119 "(validate-goto-binary)" \
121 OPT_ANSI_C_LANGUAGE \
122 OPT_RESTRICT_FUNCTION_POINTER \
123 OPT_NONDET_VOLATILE \
124 "(ensure-one-backedge-per-target)" \
Aggressive slicer Consider the control flow graph of the goto program and a criterion description of ...
void instrument_goto_program()
void do_indirect_call_and_rtti_removal(bool force=false)
bool partial_inlining_done
bool function_pointer_removal_done
virtual int doit()
invoke main modules
virtual void help()
display command line help
void register_languages()
void do_partial_inlining()
void do_remove_const_function_pointers_only()
Remove function pointers that can be resolved by analysing const variables (i.e.
goto_instrument_parse_optionst(int argc, const char **argv)
Verify and use annotated invariants and pre/post-conditions.
Count effective lines of code.
Goto Programs with Functions.
#define GOTO_INSTRUMENT_OPTIONS
Insert final assert false into a function.
Remove calls to functions without a body.
Replace calls to given functions with calls to other given functions.
Given goto functions and a list of function parameters or globals that are function pointers with lis...