use formatter in show_symbol_table

Author: Daniel Kroening

src/cbmc/cbmc_parse_options.cpp

@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language.h>
 
 #include <ansi-c/c_preprocess.h>
+#include <ansi-c/ansi_c_formatter.h>
 
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/initialize_goto_model.h>
@@ -595,7 +596,9 @@ int cbmc_parse_optionst::get_goto_program(
 
     if(cmdline.isset("show-symbol-table"))
     {
-      show_symbol_table(goto_model, ui_message_handler.get_ui());
+      namespacet ns(goto_model.symbol_table);
+      ansi_c_formattert formatter(ns);
+      show_symbol_table(goto_model, ui_message_handler.get_ui(), formatter);
       return CPROVER_EXIT_SUCCESS;
     }
 

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -21,6 +21,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/json.h>
 #include <util/exit_codes.h>
 
+#include <ansi-c/ansi_c_formatter.h>
+
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_calls_no_body.h>
@@ -463,7 +465,9 @@ int goto_instrument_parse_optionst::doit()
 
     if(cmdline.isset("show-symbol-table"))
     {
-      ::show_symbol_table(goto_model, get_ui());
+      namespacet ns(goto_model.symbol_table);
+      ansi_c_formattert formatter(ns);
+      ::show_symbol_table(goto_model, get_ui(), formatter);
       return CPROVER_EXIT_SUCCESS;
     }
 

src/goto-programs/show_symbol_table.cpp

@@ -19,13 +19,14 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_model.h"
 
-void show_symbol_table_xml_ui()
+void show_symbol_table_xml_ui(formattert &)
 {
 }
 
 void show_symbol_table_brief_plain(
   const symbol_tablet &symbol_table,
-  std::ostream &out)
+  std::ostream &out,
+  formattert &formatter)
 {
   // we want to sort alphabetically
   std::set<std::string> symbols;
@@ -41,29 +42,17 @@ void show_symbol_table_brief_plain(
   {
     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';
+      out << symbol.name << " " << formatter(symbol.type) << '\n';
+    else
+      out << symbol.name << '\n';
   }
 }
 
 void show_symbol_table_plain(
   const symbol_tablet &symbol_table,
-  std::ostream &out)
+  std::ostream &out,
+  formattert &formatter)
 {
   out << '\n' << "Symbols:" << '\n' << '\n';
 
@@ -81,35 +70,24 @@ void show_symbol_table_plain(
   {
     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)
-      throw "symbol "+id2string(symbol.name)+" has unknown mode";
-
     std::string type_str, value_str;
 
-    if(symbol.type.is_not_nil())
-      ptr->from_type(symbol.type, type_str, ns);
-
-    if(symbol.value.is_not_nil())
-      ptr->from_expr(symbol.value, value_str, ns);
-
     out << "Symbol......: " << symbol.name << '\n' << std::flush;
     out << "Pretty name.: " << symbol.pretty_name << '\n';
     out << "Module......: " << symbol.module << '\n';
     out << "Base name...: " << symbol.base_name << '\n';
     out << "Mode........: " << symbol.mode << '\n';
-    out << "Type........: " << type_str << '\n';
-    out << "Value.......: " << value_str << '\n';
+
+    out << "Type........: ";
+    if(symbol.type.is_not_nil())
+      out << formatter(symbol.type);
+    out << '\n';
+
+    out << "Value.......: ";
+    if(symbol.value.is_not_nil())
+      out << formatter(symbol.value);
+    out << '\n';
+
     out << "Flags.......:";
 
     if(symbol.is_lvalue)
@@ -146,24 +124,25 @@ void show_symbol_table_plain(
       out << " volatile";
 
     out << '\n';
-    out << "Location....: " << symbol.location << '\n';
+    out << "Location....: " << formatter(symbol.location) << '\n';
 
     out << '\n' << std::flush;
   }
 }
 
 void show_symbol_table(
   const symbol_tablet &symbol_table,
-  ui_message_handlert::uit ui)
+  ui_message_handlert::uit ui,
+  formattert &formatter)
 {
   switch(ui)
   {
   case ui_message_handlert::uit::PLAIN:
-    show_symbol_table_plain(symbol_table, std::cout);
+    show_symbol_table_plain(symbol_table, std::cout, formatter);
     break;
 
   case ui_message_handlert::uit::XML_UI:
-    show_symbol_table_xml_ui();
+    show_symbol_table_xml_ui(formatter);
     break;
 
   default:
@@ -173,23 +152,25 @@ void show_symbol_table(
 
 void show_symbol_table(
   const goto_modelt &goto_model,
-  ui_message_handlert::uit ui)
+  ui_message_handlert::uit ui,
+  formattert &formatter)
 {
-  show_symbol_table(goto_model.symbol_table, ui);
+  show_symbol_table(goto_model.symbol_table, ui, formatter);
 }
 
 void show_symbol_table_brief(
   const symbol_tablet &symbol_table,
-  ui_message_handlert::uit ui)
+  ui_message_handlert::uit ui,
+  formattert &formatter)
 {
   switch(ui)
   {
   case ui_message_handlert::uit::PLAIN:
-    show_symbol_table_brief_plain(symbol_table, std::cout);
+    show_symbol_table_brief_plain(symbol_table, std::cout, formatter);
     break;
 
   case ui_message_handlert::uit::XML_UI:
-    show_symbol_table_xml_ui();
+    show_symbol_table_xml_ui(formatter);
     break;
 
   default:
@@ -199,7 +180,8 @@ void show_symbol_table_brief(
 
 void show_symbol_table_brief(
   const goto_modelt &goto_model,
-  ui_message_handlert::uit ui)
+  ui_message_handlert::uit ui,
+  formattert &formatter)
 {
-  show_symbol_table_brief(goto_model.symbol_table, ui);
+  show_symbol_table_brief(goto_model.symbol_table, ui, formatter);
 }

src/goto-programs/show_symbol_table.h

@@ -12,25 +12,30 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_PROGRAMS_SHOW_SYMBOL_TABLE_H
 #define CPROVER_GOTO_PROGRAMS_SHOW_SYMBOL_TABLE_H
 
+#include <util/formatter.h>
 #include <util/ui_message.h>
 
 class symbol_tablet;
 class goto_modelt;
 
 void show_symbol_table(
   const symbol_tablet &,
-  ui_message_handlert::uit ui);
+  ui_message_handlert::uit ui,
+  formattert & = debug_formatter);
 
 void show_symbol_table_brief(
   const symbol_tablet &,
-  ui_message_handlert::uit ui);
+  ui_message_handlert::uit ui,
+  formattert & = debug_formatter);
 
 void show_symbol_table(
   const goto_modelt &,
-  ui_message_handlert::uit ui);
+  ui_message_handlert::uit ui,
+  formattert & = debug_formatter);
 
 void show_symbol_table_brief(
   const goto_modelt &,
-  ui_message_handlert::uit ui);
+  ui_message_handlert::uit ui,
+  formattert & = debug_formatter);
 
 #endif // CPROVER_GOTO_PROGRAMS_SHOW_SYMBOL_TABLE_H

src/jbmc/jbmc_parse_options.cpp

@@ -55,6 +55,7 @@ Author: Daniel Kroening, [email protected]
 #include <java_bytecode/convert_java_nondet.h>
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_enum_static_init_unwind_handler.h>
+#include <java_bytecode/java_formatter.h>
 #include <java_bytecode/remove_exceptions.h>
 #include <java_bytecode/remove_instanceof.h>
 #include <java_bytecode/remove_java_new.h>
@@ -671,8 +672,10 @@ int jbmc_parse_optionst::get_goto_program(
     // values, etc
     if(cmdline.isset("show-symbol-table"))
     {
+      const namespacet ns(lazy_goto_model.symbol_table);
+      java_formattert formatter(ns);
       show_symbol_table(
-        lazy_goto_model.symbol_table, ui_message_handler.get_ui());
+        lazy_goto_model.symbol_table, ui_message_handler.get_ui(), formatter);
       return 0;
     }