From b5e97ae6ebdb2328d8383a593ce7351ceafada13 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 27 Mar 2017 09:32:49 +0100 Subject: [PATCH] fixup! Add --drop-unused-functions option --- CHANGELOG | 2 ++ src/cbmc/cbmc_parse_options.cpp | 4 ++-- src/goto-instrument/goto_instrument_parse_options.cpp | 8 ++++++++ src/goto-instrument/goto_instrument_parse_options.h | 1 + src/symex/symex_parse_options.cpp | 4 ++-- 5 files changed, 15 insertions(+), 4 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index ba9ceda554..61489b8fb4 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -20,6 +20,8 @@ * GOTO-CC: GCC-style error/warning messages * GOTO-CC: New options --native-compiler and --native-linker to select the compiler/linker to be used when building combined native/goto object files. +* CBMC, SYMEX, GOTO-INSTRUMENT: New option --drop-unused-functions. Removed + ambiguous --show-reachable-properties. 5.6 diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 39a595e596..721520e48f 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -946,7 +946,7 @@ bool cbmc_parse_optionst::process_goto_program( if(cmdline.isset("drop-unused-functions")) { // Entry point will have been set before and function pointers removed - status() << "Removing Unused Functions" << eom; + status() << "Removing unused functions" << eom; remove_unused_functions(goto_functions, ui_message_handler); } @@ -1096,7 +1096,6 @@ void cbmc_parse_optionst::help() " --property id only check one specific property\n" " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*) " --trace give a counterexample trace for failed properties\n" //NOLINT(*) - " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) "\n" "C/C++ frontend options:\n" " -I path set include path (C/C++)\n" @@ -1142,6 +1141,7 @@ void cbmc_parse_optionst::help() " --show-parse-tree show parse tree\n" " --show-symbol-table show symbol table\n" HELP_SHOW_GOTO_FUNCTIONS + " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) "\n" "Program instrumentation options:\n" HELP_GOTO_CHECK diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index d2173398e4..dda6b1ea30 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -744,6 +744,14 @@ int goto_instrument_parse_optionst::doit() return 0; } + if(cmdline.isset("drop-unused-functions")) + { + do_indirect_call_and_rtti_removal(); + + status() << "Removing unused functions" << eom; + remove_unused_functions(goto_functions, get_message_handler()); + } + // write new binary? if(cmdline.args.size()==2) { diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index d3efb97576..180eeb7a2f 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -45,6 +45,7 @@ Author: Daniel Kroening, kroening@kroening.com "(stack-depth):(nondet-static)" \ "(function-enter):(function-exit):(branch):" \ OPT_SHOW_GOTO_FUNCTIONS \ + "(drop-unused-functions)" \ "(show-value-sets)" \ "(show-global-may-alias)" \ "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \ diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 5e547a19df..a3f671f0fd 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -386,7 +386,7 @@ bool symex_parse_optionst::process_goto_program(const optionst &options) if(cmdline.isset("drop-unused-functions")) { // Entry point will have been set before and function pointers removed - status() << "Removing Unused Functions" << eom; + status() << "Removing unused functions" << eom; remove_unused_functions(goto_model.goto_functions, ui_message_handler); } @@ -690,7 +690,6 @@ void symex_parse_optionst::help() " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINTNEXTLINE(whitespace/line_length) " --trace give a counterexample trace for failed properties\n" - " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) "\n" "Frontend options:\n" " -I path set include path (C/C++)\n" @@ -705,6 +704,7 @@ void symex_parse_optionst::help() " --show-parse-tree show parse tree\n" " --show-symbol-table show symbol table\n" HELP_SHOW_GOTO_FUNCTIONS + " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) " --ppc-macos set MACOS/PPC architecture\n" " --mm model set memory model (default: sc)\n" " --arch set architecture (default: "