added --show-reachable-properties

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@5164 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

src/cbmc/cbmc_parse_options.cpp

@@ -27,6 +27,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_asm.h>
+#include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/set_properties.h>
@@ -471,6 +472,18 @@ int cbmc_parse_optionst::doit()
     return 0;
   }
 
+  if(cmdline.isset("show-reachable-properties")) // may replace --show-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;
+  }
+
   if(set_properties(goto_functions))
     return 7;
 

src/cbmc/cbmc_parse_options.h

@@ -40,7 +40,7 @@ class optionst;
   "(little-endian)(big-endian)" \
   "(show-goto-functions)(show-value-sets)(show-loops)" \
   "(show-symbol-table)(show-parse-tree)(show-vcc)" \
-  "(show-claims)(claim):(show-properties)(property):" \
+  "(show-claims)(claim):(show-properties)(show-reachable-properties)(property):" \
   "(all-claims)(all-properties)" \
   "(error-label):(verbosity):(no-library)" \
   "(version)" \