cprover
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
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>
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{
129public:
130 int doit() override;
131 void help() override;
132
144
145protected:
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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.
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.