diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 9a3d00a69b4..abe3f48fa52 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -54,6 +54,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -293,6 +294,17 @@ int goto_instrument_parse_optionst::doit() return CPROVER_EXIT_SUCCESS; } + if(cmdline.isset("show-value-set-fi")) + { + namespacet ns(goto_model.symbol_table); + value_set_analysis_fit value_set( + ns, value_set_analysis_fit::track_optionst::TRACK_FUNCTION_POINTERS); + + value_set(goto_model.goto_functions); + value_set.output(goto_model.goto_functions, std::cout); + return CPROVER_EXIT_SUCCESS; + } + if(cmdline.isset("show-global-may-alias")) { do_indirect_call_and_rtti_removal(); diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index a9858a30c4a..41634566667 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -74,6 +74,7 @@ Author: Daniel Kroening, kroening@kroening.com OPT_SHOW_PROPERTIES \ "(drop-unused-functions)" \ "(show-value-sets)" \ + "(show-value-set-fi)" \ "(show-global-may-alias)" \ "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \ "(show-escape-analysis)(escape-analysis)" \