replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

fixup! Add --drop-unused-functions option

This commit is contained in:
Michael Tautschnig 2017-03-27 09:32:49 +01:00
parent d658c0c0ec
commit b5e97ae6eb
5 changed files with 15 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
CHANGELOG
View File

@ -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

4
src/cbmc/cbmc_parse_options.cpp
View File

@ -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

8
src/goto-instrument/goto_instrument_parse_options.cpp
View File

@ -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)
{

1
src/goto-instrument/goto_instrument_parse_options.h
View File

@ -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)" \

4
src/symex/symex_parse_options.cpp
View File

@ -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: "