cprover
goto_analyzer_parse_options.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto-Analyser Command Line Option Processing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
88 
89 #ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
90 #define CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
91 
92 #include <util/parse_options.h>
93 #include <util/timestamper.h>
94 #include <util/ui_message.h>
96 
97 #include <langapi/language.h>
98 
102 
103 #include <analyses/ai.h>
104 #include <analyses/goto_check.h>
105 
106 class goto_functionst;
107 class optionst;
108 
109 // clang-format off
110 #define GOTO_ANALYSER_OPTIONS_TASKS \
111  "(show)(verify)(simplify):" \
112  "(show-on-source)" \
113  "(unreachable-instructions)(unreachable-functions)" \
114  "(reachable-functions)"
115 
116 #define GOTO_ANALYSER_OPTIONS_AI \
117  "(recursive-interprocedural)" \
118  "(legacy-ait)" \
119  "(legacy-concurrent)"
120 
121 #define GOTO_ANALYSER_OPTIONS_HISTORY \
122  "(ahistorical)" \
123  "(call-stack):" \
124  "(loop-unwind):" \
125  "(branching):" \
126  "(loop-unwind-and-branching):"
127 
128 #define GOTO_ANALYSER_OPTIONS_DOMAIN \
129  "(intervals)" \
130  "(non-null)" \
131  "(constants)" \
132  "(dependence-graph)"
133 
134 #define GOTO_ANALYSER_OPTIONS_STORAGE \
135  "(one-domain-per-history)" \
136  "(one-domain-per-location)"
137 
138 #define GOTO_ANALYSER_OPTIONS_OUTPUT \
139  "(json):(xml):" \
140  "(text):(dot):"
141 
142 #define GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \
143  "(taint):(show-taint)" \
144  "(show-local-may-alias)"
145 
146 #define GOTO_ANALYSER_OPTIONS \
147  OPT_FUNCTIONS \
148  "D:I:(std89)(std99)(std11)" \
149  "(classpath):(cp):(main-class):" \
150  "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
151  "(little-endian)(big-endian)" \
152  OPT_SHOW_GOTO_FUNCTIONS \
153  OPT_SHOW_PROPERTIES \
154  OPT_GOTO_CHECK \
155  "(show-loops)" \
156  "(show-symbol-table)(show-parse-tree)" \
157  "(show-reachable-properties)(property):" \
158  "(verbosity):(version)" \
159  "(gcc)(arch):" \
160  OPT_FLUSH \
161  OPT_TIMESTAMP \
162  OPT_VALIDATE \
163  GOTO_ANALYSER_OPTIONS_TASKS \
164  "(no-simplify-slicing)" \
165  "(show-intervals)(show-non-null)" \
166  GOTO_ANALYSER_OPTIONS_AI \
167  "(location-sensitive)(concurrent)" \
168  GOTO_ANALYSER_OPTIONS_HISTORY \
169  GOTO_ANALYSER_OPTIONS_DOMAIN \
170  GOTO_ANALYSER_OPTIONS_STORAGE \
171  GOTO_ANALYSER_OPTIONS_OUTPUT \
172  GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \
173 // clang-format on
174 
176 {
177 public:
178  virtual int doit() override;
179  virtual void help() override;
180 
181  goto_analyzer_parse_optionst(int argc, const char **argv);
182 
183 protected:
185 
186  virtual void register_languages();
187 
188  virtual void get_command_line_options(optionst &options);
189 
190  virtual bool process_goto_program(const optionst &options);
191 
192  virtual int perform_analysis(const optionst &options);
193 
194  ai_baset *build_analyzer(const optionst &, const namespacet &ns);
195 };
196 
197 #endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
parse_options_baset
Definition: parse_options.h:20
optionst
Definition: options.h:23
goto_analyzer_parse_optionst::get_command_line_options
virtual void get_command_line_options(optionst &options)
Definition: goto_analyzer_parse_options.cpp:90
validation_interface.h
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition: goto_model.h:26
show_goto_functions.h
Show the goto functions.
goto_analyzer_parse_optionst::build_analyzer
ai_baset * build_analyzer(const optionst &, const namespacet &ns)
For the task, build the appropriate kind of analyzer Ideally this should be a pure function of option...
Definition: goto_analyzer_parse_options.cpp:414
goto_analyzer_parse_optionst::goto_analyzer_parse_optionst
goto_analyzer_parse_optionst(int argc, const char **argv)
Definition: goto_analyzer_parse_options.cpp:72
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_analyzer_parse_optionst::process_goto_program
virtual bool process_goto_program(const optionst &options)
Definition: goto_analyzer_parse_options.cpp:804
show_properties.h
Show the properties.
goto_analyzer_parse_optionst::doit
virtual int doit() override
invoke main modules
Definition: goto_analyzer_parse_options.cpp:520
language.h
Abstract interface to support a programming language.
goto_analyzer_parse_optionst::help
virtual void help() override
display command line help
Definition: goto_analyzer_parse_options.cpp:858
parse_options.h
goto_check.h
Program Transformation.
ai.h
Abstract Interpretation.
goto_analyzer_parse_optionst::register_languages
virtual void register_languages()
Definition: goto_analyzer_parse_options.cpp:83
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
goto_analyzer_parse_optionst
Definition: goto_analyzer_parse_options.h:176
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
timestamper.h
Emit timestamps.
goto_analyzer_parse_optionst::goto_model
goto_modelt goto_model
Definition: goto_analyzer_parse_options.h:184
goto_analyzer_parse_optionst::perform_analysis
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
Definition: goto_analyzer_parse_options.cpp:578
ui_message.h