forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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.
- Loading branch information
Showing
2 changed files
with
7 additions
and
14 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -60,7 +60,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> | ||
|
@@ -499,17 +498,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")) | ||
|
@@ -1894,6 +1886,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" | ||
|
@@ -1915,7 +1908,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" | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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 \ | ||
|