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 "(nondet-static-matching):" \
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)(slice-global-inits)" \
83 OPT_REACHABILITY_SLICER \
84 OPT_FP_REACHABILITY_SLICER \
85 "(inline)(partial-inline)(function-inline):(log):(no-caching)" \
86 "(value-set-fi-fp-removal)" \
87 OPT_REMOVE_CONST_FUNCTION_POINTERS \
88 "(print-internal-representation)" \
89 "(remove-function-pointers)" \
90 "(show-claims)(property):" \
91 "(show-symbol-table)(show-points-to)(show-rw-set)" \
93 "(show-natural-loops)(show-lexical-loops)(accelerate)(havoc-loops)" \
94 "(verbosity):(version)(xml-ui)(json-ui)" \
95 "(accelerate)(constant-propagator)" \
96 "(k-induction):(step-case)(base-case)" \
97 "(show-call-sequences)(check-call-sequence)" \
98 "(interpreter)(show-reaching-definitions)" \
99 "(list-symbols)(list-undefined-functions)" \
100 "(z3)(add-library)(show-dependence-graph)" \
101 "(horn)(skip-loops):(model-argc-argv):" \
103 "(" FLAG_LOOP_CONTRACTS ")" \
104 "(" FLAG_LOOP_CONTRACTS_NO_UNWIND ")" \
105 "(" FLAG_LOOP_CONTRACTS_FILE "):" \
106 "(" FLAG_REPLACE_CALL "):" \
107 "(" FLAG_ENFORCE_CONTRACT "):" \
108 OPT_ENFORCE_CONTRACT_REC \
109 "(show-threaded)(list-calls-args)" \
110 "(undefined-function-is-assume-false)" \
111 "(remove-function-body):"\
112 OPT_AGGRESSIVE_SLICER \
115 OPT_REMOVE_CALLS_NO_BODY \
116 OPT_REPLACE_FUNCTION_BODY \
117 OPT_GOTO_PROGRAM_STATS \
118 "(show-local-safe-pointers)(show-safe-dereferences)" \
119 "(show-sese-regions)" \
121 "(validate-goto-binary)" \
123 OPT_ANSI_C_LANGUAGE \
124 OPT_RESTRICT_FUNCTION_POINTER \
125 OPT_NONDET_VOLATILE \
126 "(ensure-one-backedge-per-target)" \
136 void help()
override;
Aggressive slicer Consider the control flow graph of the goto program and a criterion description of ...
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.
Parse and annotate contracts.
Count effective lines of code.
Main class orchestrating the the whole program transformation for function contracts with Dynamic Fra...
Documentation of Properties.
Dump C from Goto Program.
#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...
Detection for Uninitialized Local Variables.
Weak Memory Instrumentation for Threaded Goto Programs.