use format() for --show-symbol-table

regression/Makefile

@@ -7,7 +7,6 @@ DIRS = cbmc \
        goto-instrument \
        cpp \
        cbmc-cover \
-       goto-instrument-typedef \
        smt2_solver \
        strings \
        invariants \

regression/cbmc/typedef-anon-struct1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-anon-struct2/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-anon-union1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-anon-union2/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-const-struct1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-const-type1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-const-union1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-param-anon-struct1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-param-anon-union1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-param-struct1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-param-type1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-param-type2/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-param-type3/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-param-union1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-return-anon-struct1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-return-anon-union1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-return-struct1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-return-type1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-return-type2/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-return-type3/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-return-union1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-struct1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-struct2/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-type1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-type2/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-type3/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-type4/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-union1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

regression/cbmc/typedef-union2/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking

src/goto-programs/show_symbol_table.cpp

@@ -13,11 +13,10 @@ Author: Daniel Kroening, [email protected]
 
 #include <algorithm>
 #include <iostream>
-#include <memory>
-
-#include <langapi/language.h>
-#include <langapi/mode.h>
+#include <sstream>
 
+#include <util/format_expr.h>
+#include <util/format_type.h>
 #include <util/json_irep.h>
 
 #include "goto_model.h"
@@ -44,23 +43,12 @@ 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;
+    out << symbol.name;
 
     if(symbol.type.is_not_nil())
-      ptr->from_type(symbol.type, type_str, ns);
+      out << ' ' << format(symbol.type);
 
-    out << symbol.name << " " << type_str << '\n';
+    out << '\n';
   }
 }
 
@@ -84,35 +72,19 @@ 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 << format(symbol.type);
+    out << '\n';
+    out << "Value.......: ";
+    if(symbol.value.is_not_nil())
+      out << format(symbol.value);
+    out << '\n';
     out << "Flags.......:";
 
     if(symbol.is_lvalue)
@@ -172,36 +144,22 @@ static void show_symbol_table_json_ui(
   {
     const symbolt &symbol = id_and_symbol.second;
 
-    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);
-
     json_objectt symbol_json;
     symbol_json["prettyName"] = json_stringt(symbol.pretty_name);
     symbol_json["baseName"] = json_stringt(symbol.base_name);
     symbol_json["mode"] = json_stringt(symbol.mode);
     symbol_json["module"] = json_stringt(symbol.module);
 
-    symbol_json["prettyType"] = json_stringt(type_str);
-    symbol_json["prettyValue"] = json_stringt(value_str);
+    std::ostringstream type_str, value_str;
+
+    if(symbol.type.is_not_nil())
+      type_str << format(symbol.type);
+
+    if(symbol.value.is_not_nil())
+      value_str << format(symbol.value);
+
+    symbol_json["prettyType"] = json_stringt(type_str.str());
+    symbol_json["prettyValue"] = json_stringt(value_str.str());
 
     symbol_json["type"] = irep_converter.convert_from_irep(symbol.type);
     symbol_json["value"] = irep_converter.convert_from_irep(symbol.value);
@@ -247,32 +205,18 @@ static void show_symbol_table_brief_json_ui(
   {
     const symbolt &symbol = id_and_symbol.second;
 
-    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;
+    std::ostringstream type_str, value_str;
 
     if(symbol.type.is_not_nil())
-      ptr->from_type(symbol.type, type_str, ns);
+      type_str << format(symbol.type);
 
     json_objectt symbol_json;
     symbol_json["prettyName"] = json_stringt(symbol.pretty_name);
     symbol_json["baseName"] = json_stringt(symbol.base_name);
     symbol_json["mode"] = json_stringt(symbol.mode);
     symbol_json["module"] = json_stringt(symbol.module);
 
-    symbol_json["prettyType"] = json_stringt(type_str);
+    symbol_json["prettyType"] = json_stringt(type_str.str());
 
     symbol_json["type"] = irep_converter.convert_from_irep(symbol.type);
 

src/util/format_expr.cpp

@@ -280,7 +280,7 @@ std::ostream &format_rec(std::ostream &os, const exprt &expr)
               << format(to_let_expr(expr).where());
   else if(id == ID_array || id == ID_struct)
   {
-    os << "{ ";
+    os << '{';
 
     bool first = true;
 
@@ -289,12 +289,12 @@ std::ostream &format_rec(std::ostream &os, const exprt &expr)
       if(first)
         first = false;
       else
-        os << ", ";
+        os << ',';
 
-      os << format(op);
+      os << ' ' << format(op);
     }
 
-    return os << '}';
+    return os << " }";
   }
   else if(id == ID_if)
   {