Skip to content

Commit 480260a

Browse files
author
martin
committed
Move --show-intervals to goto-analyzer
There is not much to do as this is already supported, tested and documented in goto-analyzer and there are no tests for this in goto-instrument.
1 parent 98b598c commit 480260a

File tree

2 files changed

+6
-14
lines changed

2 files changed

+6
-14
lines changed

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 4 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,6 @@ Author: Daniel Kroening, [email protected]
5858
#include <analyses/escape_analysis.h>
5959
#include <analyses/global_may_alias.h>
6060
#include <analyses/interval_analysis.h>
61-
#include <analyses/interval_domain.h>
6261
#include <analyses/is_threaded.h>
6362
#include <analyses/lexical_loops.h>
6463
#include <analyses/local_bitvector_analysis.h>
@@ -487,17 +486,10 @@ int goto_instrument_parse_optionst::doit()
487486

488487
if(cmdline.isset("show-intervals"))
489488
{
490-
do_indirect_call_and_rtti_removal();
491-
492-
// recalculate numbers, etc.
493-
goto_model.goto_functions.update();
494-
495-
log.status() << "Interval Analysis" << messaget::eom;
496-
namespacet ns(goto_model.symbol_table);
497-
ait<interval_domaint> interval_analysis;
498-
interval_analysis(goto_model);
499-
interval_analysis.output(goto_model, std::cout);
500-
return CPROVER_EXIT_SUCCESS;
489+
log.status() << "--show-intervals is deprecated, "
490+
<< "use goto-analyzer --show --intervals"
491+
<< messaget::eom;
492+
return CPROVER_EXIT_USAGE_ERROR;
501493
}
502494

503495
if(cmdline.isset("show-call-sequences"))
@@ -1801,7 +1793,6 @@ void goto_instrument_parse_optionst::help()
18011793
" --show-custom-bitvector-analysis\n"
18021794
" show results of configurable bitvector analysis\n" // NOLINT(*)
18031795
" --interval-analysis perform interval analysis\n"
1804-
" --show-intervals show results of interval analysis\n"
18051796
" --show-uninitialized show maybe-uninitialized variables\n"
18061797
" --show-points-to show points-to information\n"
18071798
" --show-rw-set show read-write sets\n"

src/goto-instrument/goto_instrument_parse_options.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,7 @@ Author: Daniel Kroening, [email protected]
4848
// Options that have been moved to goto-analyzer
4949
#define GOTO_INSTRUMENT_MIGRATED_OPTIONS \
5050
"(show-dependence-graph)" \
51+
"(show-intervals)" \
5152
// empty last line
5253

5354
#define GOTO_INSTRUMENT_OPTIONS \
@@ -79,7 +80,7 @@ Author: Daniel Kroening, [email protected]
7980
"(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \
8081
"(show-escape-analysis)(escape-analysis)" \
8182
"(custom-bitvector-analysis)" \
82-
"(show-struct-alignment)(interval-analysis)(show-intervals)" \
83+
"(show-struct-alignment)(interval-analysis)" \
8384
"(show-uninitialized)(show-locations)" \
8485
"(full-slice)(reachability-slice)(slice-global-inits)" \
8586
"(fp-reachability-slice):" \

0 commit comments

Comments
 (0)