CBMC
Loading...
Searching...
No Matches
goto_instrument_parse_options.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Command Line Parsing
4
5Author: 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
28
32
33#include "aggressive_slicer.h"
34#include "count_eloc.h"
35#include "document_properties.h"
36#include "dump_c.h"
39#include "nondet_volatile.h"
40#include "reachability_slicer.h"
41#include "replace_calls.h"
42#include "uninitialized.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 "(no-unwinding-assertions)" \
64 "(log):" \
65 "(call-graph)(reachable-call-graph)" \
66 OPT_INSERT_FINAL_ASSERT_FALSE \
67 OPT_SHOW_CLASS_HIERARCHY \
68 "(isr):" \
69 "(stack-depth):(nondet-static)" \
70 "(nondet-static-exclude):" \
71 "(nondet-static-matching):" \
72 "(function-enter):(function-exit):(branch):" \
73 OPT_SHOW_GOTO_FUNCTIONS \
74 OPT_SHOW_PROPERTIES \
75 "(drop-unused-functions)" \
76 "(show-value-sets)" \
77 "(show-global-may-alias)" \
78 "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \
79 "(show-escape-analysis)(escape-analysis)" \
80 "(custom-bitvector-analysis)" \
81 "(show-struct-alignment)(interval-analysis)(show-intervals)" \
82 "(show-uninitialized)(show-locations)" \
83 "(full-slice)(slice-global-inits)" \
84 OPT_REACHABILITY_SLICER \
85 OPT_FP_REACHABILITY_SLICER \
86 "(inline)(partial-inline)(function-inline):(log):(no-caching)" \
87 "(value-set-fi-fp-removal)" \
88 OPT_REMOVE_CONST_FUNCTION_POINTERS \
89 "(print-internal-representation)" \
90 "(remove-function-pointers)" \
91 "(show-claims)(property):" \
92 "(show-symbol-table)(show-points-to)(show-rw-set)" \
93 OPT_TIMESTAMP \
94 "(show-natural-loops)(show-lexical-loops)(accelerate)(havoc-loops)" \
95 "(verbosity):(version)(xml-ui)(json-ui)" \
96 "(accelerate)(constant-propagator)" \
97 "(k-induction):(step-case)(base-case)" \
98 "(show-call-sequences)(check-call-sequence)" \
99 "(interpreter)(show-reaching-definitions)" \
100 "(list-symbols)(list-undefined-functions)" \
101 "(z3)(add-library)(show-dependence-graph)" \
102 "(horn)(skip-loops):(model-argc-argv):" \
103 OPT_DFCC \
104 "(" FLAG_LOOP_CONTRACTS ")" \
105 "(" FLAG_DISABLE_SIDE_EFFECT_CHECK ")" \
106 "(" FLAG_LOOP_CONTRACTS_NO_UNWIND ")" \
107 "(" FLAG_LOOP_CONTRACTS_FILE "):" \
108 "(" FLAG_REPLACE_CALL "):" \
109 "(" FLAG_ENFORCE_CONTRACT "):" \
110 OPT_ENFORCE_CONTRACT_REC \
111 "(show-threaded)(list-calls-args)" \
112 "(undefined-function-is-assume-false)" \
113 "(remove-function-body):" \
114 "(remove-function-body-regex):" \
115 OPT_AGGRESSIVE_SLICER \
116 OPT_FLUSH \
117 "(splice-call):" \
118 OPT_REMOVE_CALLS_NO_BODY \
119 OPT_REPLACE_FUNCTION_BODY \
120 OPT_GOTO_PROGRAM_STATS \
121 "(show-local-safe-pointers)(show-safe-dereferences)" \
122 "(show-sese-regions)" \
123 OPT_REPLACE_CALLS \
124 "(validate-goto-binary)" \
125 OPT_VALIDATE \
126 OPT_ANSI_C_LANGUAGE \
127 OPT_RESTRICT_FUNCTION_POINTER \
128 OPT_NONDET_VOLATILE \
129 "(ensure-one-backedge-per-target)" \
130 OPT_CONFIG_LIBRARY \
131 // empty last line
132
133// clang-format on
134
136{
137public:
138 int doit() override;
139 void help() override;
140
141 goto_instrument_parse_optionst(int argc, const char **argv)
144 argc,
145 argv,
146 "goto-instrument"),
150 {
151 }
152
153protected:
154 void register_languages() override;
155
156 void get_goto_program();
158
159 void do_indirect_call_and_rtti_removal(bool force=false);
161 void do_partial_inlining();
162 void do_remove_returns();
163
167
169};
170
171#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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
void help() override
display command line help
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.