12#ifndef CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
13#define CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
50#define GOTO_INSTRUMENT_OPTIONS \
51 OPT_DOCUMENT_PROPERTIES \
57 OPT_UNINITIALIZED_CHECK \
62 "(unwinding-assertions)(partial-loops)(continue-as-loops)" \
64 "(call-graph)(reachable-call-graph)" \
65 OPT_INSERT_FINAL_ASSERT_FALSE \
66 OPT_SHOW_CLASS_HIERARCHY \
68 "(stack-depth):(nondet-static)" \
69 "(nondet-static-exclude):" \
70 "(function-enter):(function-exit):(branch):" \
71 OPT_SHOW_GOTO_FUNCTIONS \
73 "(drop-unused-functions)" \
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)" \
91 "(show-natural-loops)(show-lexical-loops)(accelerate)(havoc-loops)" \
92 "(verbosity):(version)(xml-ui)(json-ui)" \
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):" \
101 "(" FLAG_LOOP_CONTRACTS ")" \
102 "(" FLAG_REPLACE_CALL "):" \
103 "(" FLAG_ENFORCE_CONTRACT "):" \
104 "(show-threaded)(list-calls-args)" \
105 "(undefined-function-is-assume-false)" \
106 "(remove-function-body):"\
107 OPT_AGGRESSIVE_SLICER \
110 OPT_REMOVE_CALLS_NO_BODY \
111 OPT_REPLACE_FUNCTION_BODY \
112 OPT_GOTO_PROGRAM_STATS \
113 "(show-local-safe-pointers)(show-safe-dereferences)" \
114 "(show-sese-regions)" \
116 "(validate-goto-binary)" \
118 OPT_ANSI_C_LANGUAGE \
119 OPT_RESTRICT_FUNCTION_POINTER \
120 OPT_NONDET_VOLATILE \
121 "(ensure-one-backedge-per-target)" \
131 void help()
override;
Aggressive slicer Consider the control flow graph of the goto program and a criterion description of ...
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
void register_languages() override
void help() override
display command line help
void instrument_goto_program()
void do_indirect_call_and_rtti_removal(bool force=false)
bool partial_inlining_done
bool function_pointer_removal_done
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)
int doit() override
invoke main modules
Verify and use annotated invariants and pre/post-conditions.
Count effective lines of code.
Documentation of Properties.
Dump C from Goto Program.
Checks for Errors in C and Java Programs.
#define GOTO_INSTRUMENT_OPTIONS
Insert final assert false into a function.
Initialize command line arguments.
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...
Detection for Uninitialized Local Variables.
Weak Memory Instrumentation for Threaded Goto Programs.