Feature filter goto symbol table [blocks: #2649]

regression/cbmc/filter_list_symbol_table/main.c

@@ -0,0 +1,7 @@
+int static_var = 15;
+
+int main()
+{
+  int b = 5 + static_var;
+  return 0;
+}

regression/cbmc/filter_list_symbol_table/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--list-symbol-table --filter-symbol-table static_lifetime,file_local
+main::1::b signed int
+return' signed int
+static_var signed int
+--
+main signed int ()

regression/cbmc/filter_list_symbols/main.c

@@ -0,0 +1,7 @@
+int static_var = 15;
+
+int main()
+{
+  int b = 5 + static_var;
+  return 0;
+}

regression/cbmc/filter_list_symbols/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--list-symbols --filter-symbol-table static_lifetime
+static_var signed int
+--
+main signed int ()
+main::1::b signed int
+return' signed int

regression/cbmc/filter_show_symbol_table/main.c

@@ -0,0 +1,7 @@
+int static_var = 15;
+
+int main()
+{
+  int b = 5 + static_var;
+  return 0;
+}

regression/cbmc/filter_show_symbol_table/test.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+--show-symbol-table --filter-symbol-table static_lifetime
+Symbol......: static_var
+Pretty name.: static_var
+Module......: main
+Base name...: static_var
+Mode........: C
+Type........: signed int
+Value.......: 15
+Flags.......: lvalue static_lifetime
+Location....: file main.c line 1
+^EXIT=0$
+^SIGNAL=0$
+--
+Symbol......: main
+Symbol......: main::1::b
+Symbol......: return'

regression/goto-instrument/filter_list_symbol_table/main.c

@@ -0,0 +1,7 @@
+int static_var = 15;
+
+int main()
+{
+  int b = 5 + static_var;
+  return 0;
+}

regression/goto-instrument/filter_list_symbol_table/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--list-symbol-table --filter-symbol-table static_lifetime
+static_var signed int
+--
+main signed int ()
+main::1::b signed int
+return' signed int

regression/goto-instrument/filter_show_symbol_table/main.c

@@ -0,0 +1,7 @@
+int static_var = 15;
+
+int main()
+{
+  int b = 5 + static_var;
+  return 0;
+}

regression/goto-instrument/filter_show_symbol_table/test.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+--show-symbol-table --filter-symbol-table static_lifetime
+Symbol......: static_var
+Pretty name.: static_var
+Module......: main
+Base name...: static_var
+Mode........: C
+Type........: signed int
+Value.......: 15
+Flags.......: lvalue static_lifetime
+Location....: file main.c line 1
+^EXIT=0$
+^SIGNAL=0$
+--
+Symbol......: main
+Symbol......: main::1::b
+Symbol......: return'

src/cbmc/cbmc_parse_options.cpp

@@ -588,10 +588,14 @@ int cbmc_parse_optionst::get_goto_program(
   {
     goto_model = initialize_goto_model(cmdline, ui_message_handler);
 
-    if(cmdline.isset("show-symbol-table"))
+    int commandline_check_return_value;
+    if(!check_commandline_for_show_symbol_flags(
+         commandline_check_return_value,
+         cmdline,
+         goto_model,
+         ui_message_handler.get_ui()))
     {
-      show_symbol_table(goto_model, ui_message_handler.get_ui());
-      return CPROVER_EXIT_SUCCESS;
+      return commandline_check_return_value;
     }
 
     if(cbmc_parse_optionst::process_goto_program(goto_model, options, log))
@@ -931,7 +935,7 @@ void cbmc_parse_optionst::help()
     "\n"
     "Program representations:\n"
     " --show-parse-tree            show parse tree\n"
-    " --show-symbol-table          show loaded symbol table\n"
+    HELP_SHOW_SYMBOL_TABLE
     HELP_SHOW_GOTO_FUNCTIONS
     " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     "\n"

src/cbmc/cbmc_parse_options.h

@@ -56,7 +56,8 @@ class optionst;
   "(little-endian)(big-endian)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \
-  "(show-symbol-table)(show-parse-tree)" \
+  OPT_SHOW_SYMBOL_TABLE \
+  "(show-parse-tree)" \
   "(drop-unused-functions)" \
   "(property):(stop-on-fail)(trace)" \
   "(error-label):(verbosity):(no-library)" \

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -462,10 +462,11 @@ int goto_instrument_parse_optionst::doit()
       return CPROVER_EXIT_SUCCESS;
     }
 
-    if(cmdline.isset("show-symbol-table"))
+    int commandline_check_return_value;
+    if(!check_commandline_for_show_symbol_flags(
+         commandline_check_return_value, cmdline, goto_model, get_ui()))
     {
-      ::show_symbol_table(goto_model, get_ui());
-      return CPROVER_EXIT_SUCCESS;
+      return commandline_check_return_value;
     }
 
     if(cmdline.isset("show-reaching-definitions"))
@@ -517,12 +518,6 @@ int goto_instrument_parse_optionst::doit()
       return CPROVER_EXIT_SUCCESS;
     }
 
-    if(cmdline.isset("list-symbols"))
-    {
-      show_symbol_table_brief(goto_model, get_ui());
-      return CPROVER_EXIT_SUCCESS;
-    }
-
     if(cmdline.isset("show-uninitialized"))
     {
       show_uninitialized(goto_model, std::cout);
@@ -1527,8 +1522,7 @@ void goto_instrument_parse_optionst::help()
     "Diagnosis:\n"
     " --show-loops                 show the loops in the program\n"
     HELP_SHOW_PROPERTIES
-    " --show-symbol-table          show loaded symbol table\n"
-    " --list-symbols               list symbols with type information\n"
+    HELP_SHOW_SYMBOL_TABLE
     HELP_SHOW_GOTO_FUNCTIONS
     HELP_GOTO_PROGRAM_STATS
     " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)

src/goto-instrument/goto_instrument_parse_options.h

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_const_function_pointers.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
+#include <goto-programs/show_symbol_table.h>
 
 #include <analyses/goto_check.h>
 
@@ -61,6 +62,7 @@ Author: Daniel Kroening, [email protected]
   "(function-enter):(function-exit):(branch):" \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \
+  OPT_SHOW_SYMBOL_TABLE \
   "(drop-unused-functions)" \
   "(show-value-sets)" \
   "(show-global-may-alias)" \
@@ -75,7 +77,7 @@ Author: Daniel Kroening, [email protected]
   "(print-internal-representation)" \
   "(remove-function-pointers)" \
   "(show-claims)(property):" \
-  "(show-symbol-table)(show-points-to)(show-rw-set)" \
+  "(show-points-to)(show-rw-set)" \
   "(cav11)" \
   OPT_TIMESTAMP \
   "(show-natural-loops)(accelerate)(havoc-loops)" \