cprover
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 <ansi-c/ansi_c_language.h>
16 
17 #include <util/config.h>
18 #include <util/parse_options.h>
19 #include <util/timestamper.h>
20 #include <util/ui_message.h>
22 
29 
30 #include <analyses/goto_check.h>
31 #include <analyses/goto_check_c.h>
32 
34 
35 #include "aggressive_slicer.h"
36 #include "contracts/contracts.h"
37 #include "count_eloc.h"
38 #include "document_properties.h"
39 #include "dump_c.h"
42 #include "model_argc_argv.h"
43 #include "nondet_volatile.h"
44 #include "replace_calls.h"
45 #include "uninitialized.h"
46 #include "unwindset.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  "(function-enter):(function-exit):(branch):" \
71  OPT_SHOW_GOTO_FUNCTIONS \
72  OPT_SHOW_PROPERTIES \
73  "(drop-unused-functions)" \
74  "(show-value-sets)" \
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)" \
90  OPT_TIMESTAMP \
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):" \
100  OPT_ARGC_ARGV \
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 \
108  OPT_FLUSH \
109  "(splice-call):" \
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)" \
115  OPT_REPLACE_CALLS \
116  "(validate-goto-binary)" \
117  OPT_VALIDATE \
118  OPT_ANSI_C_LANGUAGE \
119  OPT_RESTRICT_FUNCTION_POINTER \
120  OPT_NONDET_VOLATILE \
121  "(ensure-one-backedge-per-target)" \
122  OPT_CONFIG_LIBRARY \
123  // empty last line
124 
125 // clang-format on
126 
128 {
129 public:
130  int doit() override;
131  void help() override;
132 
133  goto_instrument_parse_optionst(int argc, const char **argv)
136  argc,
137  argv,
138  "goto-instrument"),
140  partial_inlining_done(false),
141  remove_returns_done(false)
142  {
143  }
144 
145 protected:
146  void register_languages() override;
147 
148  void get_goto_program();
150 
151  void do_indirect_call_and_rtti_removal(bool force=false);
153  void do_partial_inlining();
154  void do_remove_returns();
155 
159 
161 };
162 
163 #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.
Count effective lines of code.
Documentation of Properties.
Dump C from Goto Program.
Checks for Errors in C and Java Programs.
Program Transformation.
#define GOTO_INSTRUMENT_OPTIONS
Insert final assert false into a function.
Initialize command line arguments.
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.