brief list of symbols, from language_uit

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -41,6 +41,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/parameter_assignments.h>
 #include <goto-programs/slice_global_inits.h>
+#include <goto-programs/show_symbol_table.h>
 
 #include <pointer-analysis/value_set_analysis.h>
 #include <pointer-analysis/goto_program_dereference.h>
@@ -467,7 +468,7 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-symbol-table"))
     {
-      show_symbol_table(goto_model, get_ui());
+      ::show_symbol_table(goto_model, get_ui());
       return 0;
     }
 

src/goto-programs/show_symbol_table.cpp

@@ -23,19 +23,55 @@ void show_symbol_table_xml_ui()
 {
 }
 
+void show_symbol_table_brief_plain(
+  const symbol_tablet &symbol_table,
+  std::ostream &out)
+{
+  // we want to sort alphabetically
+  std::set<std::string> symbols;
+
+  forall_symbols(it, symbol_table.symbols)
+    symbols.insert(id2string(it->first));
+
+  const namespacet ns(symbol_table);
+
+  for(const std::string &id : symbols)
+  {
+    const symbolt &symbol=ns.lookup(id);
+
+    std::unique_ptr<languaget> ptr;
+
+    if(symbol.mode=="")
+      ptr=get_default_language();
+    else
+    {
+      ptr=get_language_from_mode(symbol.mode);
+      if(ptr==nullptr)
+        throw "symbol "+id2string(symbol.name)+" has unknown mode";
+    }
+
+    std::string type_str;
+
+    if(symbol.type.is_not_nil())
+      ptr->from_type(symbol.type, type_str, ns);
+
+    out << symbol.name << " " << type_str << '\n';
+  }
+}
+
 void show_symbol_table_plain(
-  const goto_modelt &goto_model,
+  const symbol_tablet &symbol_table,
   std::ostream &out)
 {
   out << '\n' << "Symbols:" << '\n' << '\n';
 
   // we want to sort alphabetically
   std::set<std::string> symbols;
 
-  forall_symbols(it, goto_model.symbol_table.symbols)
+  forall_symbols(it, symbol_table.symbols)
     symbols.insert(id2string(it->first));
 
-  const namespacet ns(goto_model.symbol_table);
+  const namespacet ns(symbol_table);
 
   for(const std::string &id : symbols)
   {
@@ -112,14 +148,40 @@ void show_symbol_table_plain(
   }
 }
 
+void show_symbol_table(
+  const symbol_tablet &symbol_table,
+  ui_message_handlert::uit ui)
+{
+  switch(ui)
+  {
+  case ui_message_handlert::uit::PLAIN:
+    show_symbol_table_plain(symbol_table, std::cout);
+    break;
+
+  case ui_message_handlert::uit::XML_UI:
+    show_symbol_table_xml_ui();
+    break;
+
+  default:
+    break;
+  }
+}
+
 void show_symbol_table(
   const goto_modelt &goto_model,
   ui_message_handlert::uit ui)
+{
+  show_symbol_table(goto_model.symbol_table, ui);
+}
+
+void show_symbol_table_brief(
+  const symbol_tablet &symbol_table,
+  ui_message_handlert::uit ui)
 {
   switch(ui)
   {
   case ui_message_handlert::uit::PLAIN:
-    show_symbol_table_plain(goto_model, std::cout);
+    show_symbol_table_brief_plain(symbol_table, std::cout);
     break;
 
   case ui_message_handlert::uit::XML_UI:
@@ -130,3 +192,10 @@ void show_symbol_table(
     break;
   }
 }
+
+void show_symbol_table_brief(
+  const goto_modelt &goto_model,
+  ui_message_handlert::uit ui)
+{
+  show_symbol_table_brief(goto_model.symbol_table, ui);
+}

src/goto-programs/show_symbol_table.h

@@ -14,9 +14,22 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/ui_message.h>
 
+class symbol_tablet;
 class goto_modelt;
 
 void show_symbol_table(
+  const symbol_tablet &,
+  ui_message_handlert::uit ui);
+
+void show_symbol_table_brief(
+  const symbol_tablet &,
+  ui_message_handlert::uit ui);
+
+void show_symbol_table(
+  const goto_modelt &,
+  ui_message_handlert::uit ui);
+
+void show_symbol_table_brief(
   const goto_modelt &,
   ui_message_handlert::uit ui);