CBMC
goto_instrument_parse_options.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Command Line Parsing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
13 #define CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
14 
15 #include <util/config.h>
16 #include <util/parse_options.h>
17 #include <util/timestamper.h>
18 #include <util/ui_message.h>
20 
27 
28 #include <ansi-c/ansi_c_language.h>
29 #include <ansi-c/goto_check_c.h>
31 
32 #include "aggressive_slicer.h"
33 #include "count_eloc.h"
34 #include "document_properties.h"
35 #include "dump_c.h"
38 #include "nondet_volatile.h"
39 #include "reachability_slicer.h"
40 #include "replace_calls.h"
41 #include "uninitialized.h"
42 #include "unwindset.h"
43 
44 #include "contracts/contracts.h"
47 #include "wmm/weak_memory.h"
48 
49 // clang-format off
50 #define GOTO_INSTRUMENT_OPTIONS \
51  OPT_DOCUMENT_PROPERTIES \
52  OPT_DUMP_C \
53  "(dot)(xml)" \
54  OPT_GOTO_CHECK \
55  OPT_REMOVE_POINTERS \
56  "(no-simplify)" \
57  OPT_UNINITIALIZED_CHECK \
58  OPT_WMM \
59  "(race-check)" \
60  OPT_UNWINDSET \
61  "(unwindset-file):" \
62  "(unwinding-assertions)(partial-loops)(continue-as-loops)" \
63  "(log):" \
64  "(call-graph)(reachable-call-graph)" \
65  OPT_INSERT_FINAL_ASSERT_FALSE \
66  OPT_SHOW_CLASS_HIERARCHY \
67  "(isr):" \
68  "(stack-depth):(nondet-static)" \
69  "(nondet-static-exclude):" \
70  "(nondet-static-matching):" \
71  "(function-enter):(function-exit):(branch):" \
72  OPT_SHOW_GOTO_FUNCTIONS \
73  OPT_SHOW_PROPERTIES \
74  "(drop-unused-functions)" \
75  "(show-value-sets)" \
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)" \
92  OPT_TIMESTAMP \
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):" \
102  OPT_DFCC \
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 \
113  OPT_FLUSH \
114  "(splice-call):" \
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)" \
120  OPT_REPLACE_CALLS \
121  "(validate-goto-binary)" \
122  OPT_VALIDATE \
123  OPT_ANSI_C_LANGUAGE \
124  OPT_RESTRICT_FUNCTION_POINTER \
125  OPT_NONDET_VOLATILE \
126  "(ensure-one-backedge-per-target)" \
127  OPT_CONFIG_LIBRARY \
128  // empty last line
129 
130 // clang-format on
131 
133 {
134 public:
135  int doit() override;
136  void help() override;
137 
138  goto_instrument_parse_optionst(int argc, const char **argv)
141  argc,
142  argv,
143  "goto-instrument"),
145  partial_inlining_done(false),
146  remove_returns_done(false)
147  {
148  }
149 
150 protected:
151  void register_languages() override;
152 
153  void get_goto_program();
155 
156  void do_indirect_call_and_rtti_removal(bool force=false);
158  void do_partial_inlining();
159  void do_remove_returns();
160 
164 
166 };
167 
168 #endif // CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
Aggressive slicer Consider the control flow graph of the goto program and a criterion description of ...
Class Hierarchy.
void help() override
display command line help
void do_indirect_call_and_rtti_removal(bool force=false)
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.
Program Transformation.
#define GOTO_INSTRUMENT_OPTIONS
Insert final assert false into a function.
Volatile Variables.
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...
Show the goto functions.
Show the properties.
Emit timestamps.
Detection for Uninitialized Local Variables.
Loop unwinding.
Weak Memory Instrumentation for Threaded Goto Programs.