Cover (and others) for reachable functions only

src/cbmc/cbmc_parse_options.cpp

@@ -540,19 +540,6 @@ int cbmc_parse_optionst::doit()
     return 0; // should contemplate EX_OK from sysexits.h
   }
 
-  // may replace --show-properties
-  if(cmdline.isset("show-reachable-properties"))
-  {
-    const namespacet ns(symbol_table);
-
-    // Entry point will have been set before and function pointers removed
-    status() << "Removing Unused Functions" << eom;
-    remove_unused_functions(goto_functions, ui_message_handler);
-
-    show_properties(ns, get_ui(), goto_functions);
-    return 0; // should contemplate EX_OK from sysexits.h
-  }
-
   if(set_properties(goto_functions))
     return 7; // should contemplate EX_USAGE from sysexits.h
 
@@ -952,8 +939,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 +1092,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

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

src/goto-programs/show_goto_functions.h

@@ -19,7 +19,7 @@ class goto_modelt;
   "(show-goto-functions)"
 
 #define HELP_SHOW_GOTO_FUNCTIONS \
-  " --show-goto-functions         show goto program\n"
+  " --show-goto-functions        show goto program\n"
 
 void show_goto_functions(
   const namespacet &ns,

src/symex/symex_parse_options.cpp

@@ -34,6 +34,7 @@ Author: Daniel Kroening, [email protected]
 #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)"