12#ifndef CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
13#define CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
51#define GOTO_INSTRUMENT_OPTIONS \
52 OPT_DOCUMENT_PROPERTIES \
58 OPT_UNINITIALIZED_CHECK \
63 "(unwinding-assertions)(partial-loops)(continue-as-loops)" \
64 "(no-unwinding-assertions)" \
66 "(call-graph)(reachable-call-graph)" \
67 OPT_INSERT_FINAL_ASSERT_FALSE \
68 OPT_SHOW_CLASS_HIERARCHY \
70 "(stack-depth):(nondet-static)" \
71 "(nondet-static-exclude):" \
72 "(nondet-static-matching):" \
73 "(function-enter):(function-exit):(branch):" \
74 OPT_SHOW_GOTO_FUNCTIONS \
76 "(drop-unused-functions)" \
78 "(show-global-may-alias)" \
79 "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \
80 "(show-escape-analysis)(escape-analysis)" \
81 "(custom-bitvector-analysis)" \
82 "(show-struct-alignment)(interval-analysis)(show-intervals)" \
83 "(show-uninitialized)(show-locations)" \
84 "(full-slice)(slice-global-inits)" \
85 OPT_REACHABILITY_SLICER \
86 OPT_FP_REACHABILITY_SLICER \
87 "(inline)(partial-inline)(function-inline):(log):(no-caching)" \
88 "(value-set-fi-fp-removal)" \
89 OPT_REMOVE_CONST_FUNCTION_POINTERS \
90 "(print-internal-representation)" \
91 "(remove-function-pointers)" \
92 "(show-claims)(property):" \
93 "(show-symbol-table)(show-points-to)(show-rw-set)" \
95 "(show-natural-loops)(show-lexical-loops)(accelerate)(havoc-loops)" \
96 "(verbosity):(version)(xml-ui)(json-ui)" \
97 "(accelerate)(constant-propagator)" \
98 "(k-induction):(step-case)(base-case)" \
99 "(show-call-sequences)(check-call-sequence)" \
100 "(interpreter)(show-reaching-definitions)" \
101 "(list-symbols)(list-undefined-functions)" \
102 "(z3)(add-library)(show-dependence-graph)" \
103 "(horn)(skip-loops):" \
106 "(" FLAG_LOOP_CONTRACTS ")" \
107 "(" FLAG_DISABLE_SIDE_EFFECT_CHECK ")" \
108 "(" FLAG_LOOP_CONTRACTS_NO_UNWIND ")" \
109 "(" FLAG_LOOP_CONTRACTS_FILE "):" \
110 "(" FLAG_REPLACE_CALL "):" \
111 "(" FLAG_ENFORCE_CONTRACT "):" \
112 OPT_ENFORCE_CONTRACT_REC \
113 "(show-threaded)(list-calls-args)" \
114 "(undefined-function-is-assume-false)" \
115 "(remove-function-body):"\
116 OPT_AGGRESSIVE_SLICER \
119 OPT_REMOVE_CALLS_NO_BODY \
120 OPT_REPLACE_FUNCTION_BODY \
121 OPT_GOTO_PROGRAM_STATS \
122 "(show-local-safe-pointers)(show-safe-dereferences)" \
123 "(show-sese-regions)" \
125 "(validate-goto-binary)" \
127 OPT_ANSI_C_LANGUAGE \
128 OPT_RESTRICT_FUNCTION_POINTER \
129 OPT_NONDET_VOLATILE \
130 "(ensure-one-backedge-per-target)" \
140 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.
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.