Add --drop-unused-functions option

The default behaviour of CBMC for the options --show-goto-functions,
--show-properties and --cover is to consider all functions. This
is particularly annoying for --cover where coverage goals are
reported from functions that are trivially unreachable from the entry point.
Also, --show-reachable-properties has been introduced in the past
to hide such properties.
We could change the default behaviour to slicing away everything
that is trivially unreachable from the entry point. However, this would
require an extra option to be able to view all functions and properties.
This commit preserves the default behaviour and enables focussing
the output of --show-goto-functions --show-properties and --cover
on functions that are not trivially unreachable using --drop-unused-functions.

src/cbmc/cbmc_parse_options.cpp

@@ -952,8 +952,14 @@ bool cbmc_parse_optionst::process_goto_program(
     // add loop ids
     goto_functions.compute_loop_numbers();
 
-    // instrument cover goals
+    if(cmdline.isset("drop-unused-functions"))
+    {
+      // Entry point will have been set before and function pointers removed
+      status() << "Removing Unused Functions" << eom;
+      remove_unused_functions(goto_functions, ui_message_handler);
+    }
 
+    // instrument cover goals
     if(cmdline.isset("cover"))
     {
       std::list<std::string> criteria_strings=
@@ -1099,6 +1105,7 @@ 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"

src/cbmc/cbmc_parse_options.h

@@ -42,6 +42,7 @@ class optionst;
   "(show-goto-functions)(show-loops)" \
   "(show-symbol-table)(show-parse-tree)(show-vcc)" \
   "(show-claims)(claim):(show-properties)(show-reachable-properties)" \
+  "(drop-unused-functions)" \
   "(property):(stop-on-fail)(trace)" \
   "(error-label):(verbosity):(no-library)" \
   "(nondet-static)" \

src/symex/symex_parse_options.cpp

@@ -34,6 +34,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_exceptions.h>
 #include <goto-programs/remove_instanceof.h>
+#include <goto-programs/remove_unused_functions.h>
 
 #include <goto-symex/rewrite_union.h>
 #include <goto-symex/adjust_float_expressions.h>
@@ -383,6 +384,13 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
     // add loop ids
     goto_model.goto_functions.compute_loop_numbers();
 
+    if(cmdline.isset("drop-unused-functions"))
+    {
+      // Entry point will have been set before and function pointers removed
+      status() << "Removing Unused Functions" << eom;
+      remove_unused_functions(goto_model.goto_functions, ui_message_handler);
+    }
+
     if(cmdline.isset("cover"))
     {
       std::string criterion=cmdline.get_value("cover");
@@ -683,6 +691,7 @@ 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"

src/symex/symex_parse_options.h

@@ -41,6 +41,7 @@ class optionst;
   "(string-abstraction)(no-arch)(arch):(floatbv)(fixedbv)" \
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
   "(show-locs)(show-vcc)(show-properties)" \
+  "(drop-unused-functions)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   "(property):(trace)(show-trace)(stop-on-fail)(eager-infeasibility)" \
   "(no-simplify)(no-unwinding-assertions)(no-propagation)"