Skip to content

Commit e936c50

Browse files
author
martin
committed
Convert --intervals and --non-null from being specific to general analysis.
This may change the text output slightly but the core functionality remains the same for intervals. Non-null only existed as an option and wasn't actually implemented, so it is disabled for now, with the options resulting in a more helpful error message. Also this deprecates static_analyzer.{h,cpp} as the only use in the main code-base has been replaced by static_show_domain.
1 parent f79b73e commit e936c50

File tree

4 files changed

+64
-37
lines changed

4 files changed

+64
-37
lines changed

‎src/goto-analyzer/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
SRC = goto_analyzer_main.cpp \
22
goto_analyzer_parse_options.cpp \
3-
static_analyzer.cpp \
43
taint_analysis.cpp \
54
taint_parser.cpp \
65
unreachable_instructions.cpp \

‎src/goto-analyzer/goto_analyzer_parse_options.cpp

+58-36
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,7 @@ Author: Daniel Kroening, [email protected]
4343
#include <analyses/local_may_alias.h>
4444
#include <analyses/constant_propagator.h>
4545
#include <analyses/dependence_graph.h>
46+
#include <analyses/interval_domain.h>
4647

4748
#include <langapi/mode.h>
4849

@@ -57,7 +58,6 @@ Author: Daniel Kroening, [email protected]
5758

5859
#include "taint_analysis.h"
5960
#include "unreachable_instructions.h"
60-
#include "static_analyzer.h"
6161
#include "static_show_domain.h"
6262
#include "static_simplifier.h"
6363
#include "static_verifier.h"
@@ -161,21 +161,6 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
161161
options.set_option("reachable-functions", true);
162162
options.set_option("specific-analysis", true);
163163
}
164-
if(cmdline.isset("intervals"))
165-
{
166-
options.set_option("intervals", true);
167-
options.set_option("specific-analysis", true);
168-
}
169-
if(cmdline.isset("show-intervals"))
170-
{
171-
options.set_option("show-intervals", true);
172-
options.set_option("specific-analysis", true);
173-
}
174-
if(cmdline.isset("non-null"))
175-
{
176-
options.set_option("non-null", true);
177-
options.set_option("specific-analysis", true);
178-
}
179164
if(cmdline.isset("show-local-may-alias"))
180165
{
181166
options.set_option("show-local-may-alias", true);
@@ -236,7 +221,28 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
236221
"simplify-slicing",
237222
!(cmdline.isset("no-simplify-slicing")));
238223
}
239-
224+
else if(cmdline.isset("show-intervals"))
225+
{
226+
// For backwards compatibility
227+
options.set_option("show", true);
228+
options.set_option("general-analysis", true);
229+
options.set_option("intervals", true);
230+
options.set_option("domain set", true);
231+
}
232+
else if(cmdline.isset("(show-non-null)"))
233+
{
234+
// For backwards compatibility
235+
options.set_option("show", true);
236+
options.set_option("general-analysis", true);
237+
options.set_option("non-null", true);
238+
options.set_option("domain set", true);
239+
}
240+
else if(cmdline.isset("intervals") || cmdline.isset("non-null"))
241+
{
242+
// For backwards compatibility either of these on their own means show
243+
options.set_option("show", true);
244+
options.set_option("general-analysis", true);
245+
}
240246

241247
if (options.get_bool_option("general-analysis"))
242248
{
@@ -263,6 +269,17 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
263269
options.set_option("dependence-graph", true);
264270
options.set_option("domain set", true);
265271
}
272+
else if(cmdline.isset("intervals"))
273+
{
274+
options.set_option("intervals", true);
275+
options.set_option("domain set", true);
276+
}
277+
else if(cmdline.isset("non-null"))
278+
{
279+
options.set_option("non-null", true);
280+
options.set_option("domain set", true);
281+
}
282+
266283

267284
if(!options.get_bool_option("domain set"))
268285
{
@@ -291,6 +308,17 @@ ai_baset *goto_analyzer_parse_optionst::build_analyzer(const optionst &options)
291308
{
292309
domain=new dependence_grapht(namespacet(goto_model.symbol_table));
293310
}
311+
else if(options.get_bool_option("intervals"))
312+
{
313+
domain=new ait<interval_domaint>();
314+
}
315+
#if 0
316+
// Not actually implemented, despite the option...
317+
else if(options.get_bool_option("non-null"))
318+
{
319+
domain=new ait<non_null_domaint>();
320+
}
321+
#endif
294322
}
295323
else if(options.get_bool_option("concurrent"))
296324
{
@@ -304,6 +332,17 @@ ai_baset *goto_analyzer_parse_optionst::build_analyzer(const optionst &options)
304332
{
305333
domain=new dependence_grapht(namespacet(goto_model.symbol_table));
306334
}
335+
else if(options.get_bool_option("intervals"))
336+
{
337+
domain=new concurrency_aware_ait<interval_domaint>();
338+
}
339+
#if 0
340+
// Not actually implemented, despite the option...
341+
else if(options.get_bool_option("non-null"))
342+
{
343+
domain=new concurrency_aware_ait<non_null_domaint>();
344+
}
345+
#endif
307346
#endif
308347
}
309348

@@ -529,23 +568,6 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
529568
if(set_properties())
530569
return 7;
531570

532-
if(options.get_bool_option("show-intervals"))
533-
{
534-
show_intervals(goto_model, std::cout);
535-
return 0;
536-
}
537-
538-
if(options.get_bool_option("non-null") ||
539-
options.get_bool_option("intervals"))
540-
{
541-
optionst options;
542-
options.set_option("json", cmdline.get_value("json"));
543-
options.set_option("xml", cmdline.get_value("xml"));
544-
bool result=
545-
static_analyzer(goto_model, options, get_message_handler());
546-
return result?10:0;
547-
}
548-
549571
if(options.get_bool_option("general-analysis"))
550572
{
551573

@@ -760,6 +782,8 @@ void goto_analyzer_parse_optionst::help()
760782
"\n"
761783
"Domain options:\n"
762784
" --constants constant domain\n"
785+
" --intervals interval domain\n"
786+
" --non-null non-null domain\n"
763787
" --dependence-graph data and control dependencies between instructions\n" // NOLINT(*)
764788
"\n"
765789
"Output options:\n"
@@ -777,8 +801,6 @@ void goto_analyzer_parse_optionst::help()
777801
" --unreachable-functions list functions unreachable from the entry point\n"
778802
// NOLINTNEXTLINE(whitespace/line_length)
779803
" --reachable-functions list functions reachable from the entry point\n"
780-
" --intervals interval analysis\n"
781-
" --non-null non-null analysis\n"
782804
"\n"
783805
"C/C++ frontend options:\n"
784806
" -I path set include path (C/C++)\n"

‎src/goto-analyzer/static_analyzer.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,9 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9+
#define USE_DEPRECATED_STATIC_ANALYZER_H
910
#include "static_analyzer.h"
11+
#undef USE_DEPRECATED_STATIC_ANALYZER_H
1012

1113
#include <fstream>
1214

‎src/goto-analyzer/static_analyzer.h

+4
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,10 @@ Author: Daniel Kroening, [email protected]
1010
#ifndef CPROVER_GOTO_ANALYZER_STATIC_ANALYZER_H
1111
#define CPROVER_GOTO_ANALYZER_STATIC_ANALYZER_H
1212

13+
#ifndef USE_DEPRECATED_STATIC_ANALYZER_H
14+
#error Deprecated, use static_show_domain.h instead
15+
#endif
16+
1317
#include <iosfwd>
1418

1519
#include <util/message.h>

0 commit comments

Comments
 (0)