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.

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -55,7 +55,6 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/global_may_alias.h>
 #include <analyses/guard.h>
 #include <analyses/interval_analysis.h>
-#include <analyses/interval_domain.h>
 #include <analyses/is_threaded.h>
 #include <analyses/lexical_loops.h>
 #include <analyses/local_bitvector_analysis.h>
@@ -495,17 +494,10 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-intervals"))
     {
-      do_indirect_call_and_rtti_removal();
-
-      // recalculate numbers, etc.
-      goto_model.goto_functions.update();
-
-      log.status() << "Interval Analysis" << messaget::eom;
-      namespacet ns(goto_model.symbol_table);
-      ait<interval_domaint> interval_analysis;
-      interval_analysis(goto_model);
-      interval_analysis.output(goto_model, std::cout);
-      return CPROVER_EXIT_SUCCESS;
+      log.status() << "--show-intervals is deprecated, "
+                   << "use goto-analyzer --show --intervals"
+                   << messaget::eom;
+      return CPROVER_EXIT_USAGE_ERROR;
     }
 
     if(cmdline.isset("show-call-sequences"))
@@ -1893,6 +1885,7 @@ void goto_instrument_parse_optionst::help()
     " {y--interpreter} \t do concrete execution\n"
     "\n"
     "Data-flow analyses:\n"
+<<<<<<< HEAD
 <<<<<<< HEAD
     " {y--show-struct-alignment} \t show struct members that might be"
     " concurrently accessed\n"
@@ -1914,7 +1907,6 @@ void goto_instrument_parse_optionst::help()
     " {y--show-custom-bitvector-analysis} \t show results of configurable"
     " bitvector analysis\n"
     " {y--interval-analysis} \t perform interval analysis\n"
-    " {y--show-intervals} \t show results of interval analysis\n"
     " {y--show-uninitialized} \t show maybe-uninitialized variables\n"
     " {y--show-points-to} \t show points-to information\n"
     " {y--show-rw-set} \t show read-write sets\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -50,6 +50,7 @@ Author: Daniel Kroening, [email protected]
 // Options that have been moved to goto-analyzer
 #define GOTO_INSTRUMENT_MIGRATED_OPTIONS \
   "(show-dependence-graph)" \
+  "(show-intervals)" \
   // empty last line
 
 #define GOTO_INSTRUMENT_OPTIONS                 \
@@ -82,7 +83,7 @@ Author: Daniel Kroening, [email protected]
   "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \
   "(show-escape-analysis)(escape-analysis)" \
   "(custom-bitvector-analysis)" \
-  "(show-struct-alignment)(interval-analysis)(show-intervals)" \
+  "(show-struct-alignment)(interval-analysis)" \
   "(show-uninitialized)(show-locations)" \
   "(full-slice)(slice-global-inits)" \
   OPT_REACHABILITY_SLICER \