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/goto_check.h>
105 
106 class optionst;
107 
108 // clang-format off
109 #define GOTO_ANALYSER_OPTIONS_TASKS \
110  "(show)(verify)(simplify):" \
111  "(show-on-source)" \
112  "(unreachable-instructions)(unreachable-functions)" \
113  "(reachable-functions)"
114 
115 #define GOTO_ANALYSER_OPTIONS_AI \
116  "(recursive-interprocedural)" \
117  "(three-way-merge)" \
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  "(vsd)(variable-sensitivity)" \
134  "(dependence-graph-vs)" \
135 
136 #define GOTO_ANALYSER_OPTIONS_STORAGE \
137  "(one-domain-per-history)" \
138  "(one-domain-per-location)"
139 
140 #define GOTO_ANALYSER_OPTIONS_OUTPUT \
141  "(json):(xml):" \
142  "(text):(dot):"
143 
144 #define GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \
145  "(taint):(show-taint)" \
146  "(show-local-may-alias)"
147 
148 #define GOTO_ANALYSER_OPTIONS \
149  OPT_FUNCTIONS \
150  OPT_CONFIG_C_CPP \
151  OPT_CONFIG_PLATFORM \
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  OPT_FLUSH \
160  OPT_TIMESTAMP \
161  OPT_VALIDATE \
162  GOTO_ANALYSER_OPTIONS_TASKS \
163  "(no-simplify-slicing)" \
164  "(show-intervals)(show-non-null)" \
165  GOTO_ANALYSER_OPTIONS_AI \
166  "(location-sensitive)(concurrent)" \
167  GOTO_ANALYSER_OPTIONS_HISTORY \
168  GOTO_ANALYSER_OPTIONS_DOMAIN \
169  OPT_VSD \
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  void register_languages() override;
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 
195 #endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
virtual int doit() override
invoke main modules
virtual void get_command_line_options(optionst &options)
goto_analyzer_parse_optionst(int argc, const char **argv)
virtual bool process_goto_program(const optionst &options)
virtual int perform_analysis(const optionst &options)
Depending on the command line mode, run one of the analysis tasks.
virtual void help() override
display command line help
Program Transformation.
Symbol Table + CFG.
Abstract interface to support a programming language.
Show the goto functions.
Show the properties.
Emit timestamps.
There are different ways of handling arrays, structures, unions and pointers.