Revert security-scanner version of recording symbol table

Go back to non-virtual symbol_tablet

Author: NathanJPhillips

src/analyses/is_threaded.cpp

@@ -85,7 +85,7 @@ class is_threaded_domaint:public ai_domain_baset
 void is_threadedt::compute(const goto_functionst &goto_functions)
 {
   // the analysis doesn't actually use the namespace, fake one
-  concrete_symbol_tablet symbol_table;
+  symbol_tablet symbol_table;
   const namespacet ns(symbol_table);
 
   ait<is_threaded_domaint> is_threaded_analysis;

src/ansi-c/ansi_c_language.cpp

@@ -106,7 +106,7 @@ bool ansi_c_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module)
 {
-  concrete_symbol_tablet new_symbol_table;
+  symbol_tablet new_symbol_table;
 
   if(ansi_c_typecheck(
     parse_tree,

src/ansi-c/ansi_c_typecheck.cpp

@@ -42,7 +42,7 @@ bool ansi_c_typecheck(
   const unsigned errors_before=
     message_handler.get_message_count(messaget::M_ERROR);
 
-  concrete_symbol_tablet symbol_table;
+  symbol_tablet symbol_table;
   ansi_c_parse_treet ansi_c_parse_tree;
 
   ansi_c_typecheckt ansi_c_typecheck(

src/ansi-c/type2name.cpp

@@ -269,6 +269,6 @@ std::string type2name(const typet &type, const namespacet &ns)
 
 std::string type2name(const typet &type)
 {
-  concrete_symbol_tablet symbol_table;
+  symbol_tablet symbol_table;
   return type2name(type, namespacet(symbol_table));
 }

src/cbmc/bmc.h

@@ -68,7 +68,7 @@ class bmct:public safety_checkert
 
 protected:
   const optionst &options;
-  concrete_symbol_tablet new_symbol_table;
+  symbol_tablet new_symbol_table;
   namespacet ns;
   symex_target_equationt equation;
   symex_bmct symex;

src/cpp/cpp_language.cpp

@@ -126,7 +126,7 @@ bool cpp_languaget::typecheck(
   if(module=="")
     return false;
 
-  concrete_symbol_tablet new_symbol_table;
+  symbol_tablet new_symbol_table;
 
   if(cpp_typecheck(
       cpp_parse_tree, new_symbol_table, module, get_message_handler()))

src/cpp/cpp_typecheck.cpp

@@ -102,7 +102,7 @@ bool cpp_typecheck(
   const unsigned errors_before=
     message_handler.get_message_count(messaget::M_ERROR);
 
-  concrete_symbol_tablet symbol_table;
+  symbol_tablet symbol_table;
   cpp_parse_treet cpp_parse_tree;
 
   cpp_typecheckt cpp_typecheck(cpp_parse_tree, symbol_table,

src/goto-cc/linker_script_merge.cpp

@@ -53,7 +53,7 @@ int linker_script_merget::add_linker_script_definitions()
     return fail;
   }
 
-  concrete_symbol_tablet original_st;
+  symbol_tablet original_st;
   goto_functionst original_gf;
   fail=read_goto_binary(goto_file, original_st, original_gf,
       get_message_handler());

src/goto-instrument/dump_c.cpp

@@ -46,7 +46,7 @@ void dump_ct::operator()(std::ostream &os)
 
   // add copies of struct types when ID_C_transparent_union is only
   // annotated to parameter
-  concrete_symbol_tablet symbols_transparent;
+  symbol_tablet symbols_transparent;
   for(const auto &named_symbol : copied_symbol_table.symbols)
   {
     const symbolt &symbol=named_symbol.second;

src/goto-instrument/dump_c_class.h

@@ -48,7 +48,7 @@ class dump_ct
 
 protected:
   const goto_functionst &goto_functions;
-  concrete_symbol_tablet copied_symbol_table;
+  symbol_tablet copied_symbol_table;
   const namespacet ns;
   std::unique_ptr<languaget> language;
   const bool harness;

src/goto-instrument/model_argc_argv.cpp

@@ -106,7 +106,7 @@ bool model_argc_argv(
   ansi_c_language.parse(iss, "");
   config.ansi_c.preprocessor=pp;
 
-  concrete_symbol_tablet tmp_symbol_table;
+  symbol_tablet tmp_symbol_table;
   ansi_c_language.typecheck(tmp_symbol_table, "<built-in-library>");
 
   goto_programt init_instructions;

src/goto-programs/goto_model.h

@@ -22,7 +22,7 @@ Author: Daniel Kroening, [email protected]
 class goto_modelt
 {
 public:
-  concrete_symbol_tablet symbol_table;
+  symbol_tablet symbol_table;
   goto_functionst goto_functions;
 
   void clear()

src/goto-programs/goto_program_template.h

@@ -495,7 +495,7 @@ class goto_program_templatet
   /// Output goto-program to given stream
   std::ostream &output(std::ostream &out) const
   {
-    return output(namespacet(concrete_symbol_tablet()), "", out);
+    return output(namespacet(symbol_tablet()), "", out);
   }
 
   /// Output a single instruction

src/goto-programs/read_goto_binary.cpp

@@ -251,7 +251,7 @@ bool read_object_and_link(
 /// \return true on error, false otherwise
 bool read_object_and_link(
   const std::string &file_name,
-  concrete_symbol_tablet &dest_symbol_table,
+  symbol_tablet &dest_symbol_table,
   goto_functionst &dest_functions,
   message_handlert &message_handler)
 {

src/goto-programs/read_goto_binary.h

@@ -18,7 +18,7 @@ class goto_functionst;
 class goto_modelt;
 class message_handlert;
 class symbol_tablet;
-class concrete_symbol_tablet;
+class symbol_tablet;
 
 bool read_goto_binary(
   const std::string &filename,
@@ -35,7 +35,7 @@ bool is_goto_binary(const std::string &filename);
 
 bool read_object_and_link(
   const std::string &file_name,
-  concrete_symbol_tablet &,
+  symbol_tablet &,
   goto_functionst &,
   message_handlert &);
 

src/goto-symex/symex_target_equation.cpp

@@ -723,7 +723,7 @@ std::ostream &operator<<(
   const symex_target_equationt::SSA_stept &step)
 {
   // may cause lookup failures, since it's blank
-  concrete_symbol_tablet symbol_table;
+  symbol_tablet symbol_table;
   namespacet ns(symbol_table);
   step.output(ns, out);
   return out;

src/java_bytecode/java_bytecode_parse_tree.cpp

@@ -83,7 +83,7 @@ void java_bytecode_parse_treet::classt::output(std::ostream &out) const
 
 void java_bytecode_parse_treet::annotationt::output(std::ostream &out) const
 {
-  concrete_symbol_tablet symbol_table;
+  symbol_tablet symbol_table;
   namespacet ns(symbol_table);
 
   out << '@' << type2java(type, ns);
@@ -109,7 +109,7 @@ void java_bytecode_parse_treet::annotationt::output(std::ostream &out) const
 void java_bytecode_parse_treet::annotationt::element_value_pairt::output(
   std::ostream &out) const
 {
-  concrete_symbol_tablet symbol_table;
+  symbol_tablet symbol_table;
   namespacet ns(symbol_table);
 
   out << '"' << element_name << '"' << '=';
@@ -118,7 +118,7 @@ void java_bytecode_parse_treet::annotationt::element_value_pairt::output(
 
 void java_bytecode_parse_treet::methodt::output(std::ostream &out) const
 {
-  concrete_symbol_tablet symbol_table;
+  symbol_tablet symbol_table;
   namespacet ns(symbol_table);
 
   for(const auto &annotation : annotations)

src/jsil/jsil_language.cpp

@@ -152,7 +152,7 @@ bool jsil_languaget::to_expr(
     result=true;
   else
   {
-    concrete_symbol_tablet symbol_table;
+    symbol_tablet symbol_table;
     result=
       jsil_convert(parse_tree, symbol_table, get_message_handler());
 

src/jsil/jsil_typecheck.cpp

@@ -925,7 +925,7 @@ bool jsil_typecheck(
   const unsigned errors_before=
     message_handler.get_message_count(messaget::M_ERROR);
 
-  concrete_symbol_tablet symbol_table;
+  symbol_tablet symbol_table;
 
   jsil_typecheckt jsil_typecheck(
     symbol_table,

src/langapi/language_ui.h

@@ -21,7 +21,7 @@ class language_uit:public messaget
 {
 public:
   language_filest language_files;
-  concrete_symbol_tablet symbol_table;
+  symbol_tablet symbol_table;
 
   language_uit(
     const cmdlinet &cmdline,

src/langapi/language_util.cpp

@@ -153,13 +153,13 @@ std::string type_to_name(
 
 std::string from_expr(const exprt &expr)
 {
-  concrete_symbol_tablet symbol_table;
+  symbol_tablet symbol_table;
   return from_expr(namespacet(symbol_table), "", expr);
 }
 
 std::string from_type(const typet &type)
 {
-  concrete_symbol_tablet symbol_table;
+  symbol_tablet symbol_table;
   return from_type(namespacet(symbol_table), "", type);
 }
 
@@ -185,6 +185,6 @@ exprt to_expr(
 
 std::string type_to_name(const typet &type)
 {
-  concrete_symbol_tablet symbol_table;
+  symbol_tablet symbol_table;
   return type_to_name(namespacet(symbol_table), "", type);
 }

src/pointer-analysis/goto_program_dereference.cpp

@@ -436,7 +436,7 @@ void dereference(
   value_setst &value_sets)
 {
   optionst options;
-  concrete_symbol_tablet new_symbol_table;
+  symbol_tablet new_symbol_table;
   goto_program_dereferencet
     goto_program_dereference(ns, new_symbol_table, options, value_sets);
   goto_program_dereference.dereference_expression(target, expr);