templates now use proper suffixes

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@5667 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

src/cpp/cpp_id.cpp

@@ -83,6 +83,9 @@ void cpp_idt::print_fields(std::ostream &out, unsigned indent) const
   for(unsigned i=0; i<indent; i++) out << ' ';
   out << "  prefix=" << prefix << std::endl;
 
+  for(unsigned i=0; i<indent; i++) out << ' ';
+  out << "  suffix=" << suffix << std::endl;
+
   for(unsigned i=0; i<indent; i++) out << ' ';
   out << "  base_name=" << base_name << std::endl;
 

src/cpp/cpp_id.h

@@ -59,15 +59,15 @@ class cpp_idt
   {
     return id_class==TYPEDEF;
   }
-
+  
   irep_idt identifier, base_name;
 
   // if it is a member or method, what class is it in?
   irep_idt class_identifier;
   exprt this_expr;
 
   // scope data
-  std::string prefix;
+  std::string prefix, suffix;
   unsigned compound_counter;
 
   cpp_idt &insert(const irep_idt &_base_name)

src/cpp/cpp_instantiate_template.cpp

@@ -163,8 +163,8 @@ const symbolt &cpp_typecheckt::class_template_symbol(
 
   irep_idt identifier=
     id2string(template_scope->prefix)+
-    id2string(suffix)+
-    "tag-"+id2string(template_symbol.base_name);
+    "tag-"+id2string(template_symbol.base_name)+
+    id2string(suffix);
 
   // already there?
   symbol_tablet::symbolst::const_iterator s_it=symbol_table.symbols.find(identifier);
@@ -317,7 +317,7 @@ const symbolt &cpp_typecheckt::instantiate_template(
   if(template_scope==NULL)
   {
     err_location(source_location);
-    str << "identifier: " << template_symbol.name << std::endl;
+    str << "identifier: " << template_symbol.name << '\n';
     throw "template instantiation error: scope not found";
   }
 
@@ -391,16 +391,17 @@ const symbolt &cpp_typecheckt::instantiate_template(
   else
   {
     // set up a scope as subscope of the template scope
-    std::string prefix=template_scope->get_parent().prefix+suffix;
     cpp_scopet &sub_scope=
       cpp_scopes.current_scope().new_scope(subscope_name);
-    sub_scope.prefix=prefix;
+    sub_scope.id_class=cpp_idt::TEMPLATE_SCOPE;
+    sub_scope.prefix=template_scope->get_parent().prefix;
+    sub_scope.suffix=suffix;
     sub_scope.add_using_scope(template_scope->get_parent());
     cpp_scopes.go_to(sub_scope);
     cpp_scopes.id_map.insert(
       cpp_scopest::id_mapt::value_type(subscope_name, &sub_scope));
   }
-
+  
   // store the information that the template has
   // been instantiated using these arguments
   {

src/cpp/cpp_scope.h

@@ -55,6 +55,11 @@ class cpp_scopet:public cpp_idt
            id_class==NAMESPACE;
   }
 
+  inline bool is_template_scope() const
+  {
+    return id_class==TEMPLATE_SCOPE;
+  }
+
   cpp_scopet &get_parent() const
   {
     return static_cast<cpp_scopet &>(cpp_idt::get_parent());
@@ -82,8 +87,7 @@ class cpp_scopet:public cpp_idt
     using_scopes.push_back(&other);
   }
 
-  class cpp_scopet &new_scope(
-    const irep_idt &new_scope_name);
+  class cpp_scopet &new_scope(const irep_idt &new_scope_name);
 };
 
 class cpp_root_scopet:public cpp_scopet

src/cpp/cpp_scopes.cpp

@@ -27,9 +27,7 @@ Function: cpp_scopest::new_block_scope
 cpp_scopet &cpp_scopest::new_block_scope()
 {
   unsigned prefix=++current_scope().compound_counter;
-  cpp_scopet &n=new_scope(i2string(prefix));
-  n.id_class=cpp_idt::BLOCK_SCOPE;
-  return n;
+  return new_scope(i2string(prefix), cpp_idt::BLOCK_SCOPE);
 }
 
 /*******************************************************************\

src/cpp/cpp_scopes.h

@@ -20,33 +20,34 @@ Author: Daniel Kroening, [email protected]
 class cpp_scopest
 {
 public:
-  cpp_scopest()
+  inline cpp_scopest()
   {
     current_scope_ptr=&root_scope;
   }
 
   typedef std::set<cpp_scopet *> scope_sett;
   typedef std::set<cpp_idt *> id_sett;
 
-  cpp_scopet &current_scope()
+  inline cpp_scopet &current_scope()
   {
     return *current_scope_ptr;
   }
 
-  cpp_scopet &new_scope(const irep_idt &new_scope_name)
+  cpp_scopet &new_scope(
+    const irep_idt &new_scope_name,
+    cpp_idt::id_classt id_class)
   {
     assert(!new_scope_name.empty());
     cpp_scopet &n=current_scope_ptr->new_scope(new_scope_name);
+    n.id_class=id_class;
     id_map[n.identifier]=&n;
     current_scope_ptr=&n;
     return n;
   }
 
-  cpp_scopet &new_namespace(const irep_idt &new_scope_name)
+  inline cpp_scopet &new_namespace(const irep_idt &new_scope_name)
   {
-    cpp_scopet &n=new_scope(new_scope_name);
-    n.id_class=cpp_idt::NAMESPACE;
-    return n;
+    return new_scope(new_scope_name, cpp_idt::NAMESPACE);
   }
 
   cpp_scopet &new_block_scope();

src/cpp/cpp_typecheck_compound_type.cpp

@@ -191,14 +191,15 @@ void cpp_typecheckt::typecheck_compound_type(
       dest_scope=&cpp_typecheck_resolve.resolve_scope(cpp_name, base_name, t_args);
     }
   }
-
+  
   // The identifier 'tag-X' matches what the C front-end does!
   // The hypen is deliberate to avoid collisions with other
   // identifiers.
   const irep_idt symbol_name=
     dest_scope->prefix+
-    "tag-"+id2string(base_name);
-
+    "tag-"+id2string(base_name)+
+    dest_scope->suffix;
+    
   // check if we have it already
 
   symbol_tablet::symbolst::iterator previous_symbol=
@@ -207,7 +208,7 @@ void cpp_typecheckt::typecheck_compound_type(
   if(previous_symbol!=symbol_table.symbols.end())
   {
     // we do!
-
+    
     symbolt &symbol=previous_symbol->second;
 
     if(has_body)
@@ -247,8 +248,11 @@ void cpp_typecheckt::typecheck_compound_type(
     symbol.type.swap(type);
     symbol.is_type=true;
     symbol.is_macro=false;
-    symbol.pretty_name=cpp_scopes.current_scope().prefix+id2string(symbol.base_name);
-    symbol.type.set(ID_tag, symbol.pretty_name);
+    symbol.pretty_name=
+      cpp_scopes.current_scope().prefix+
+      id2string(symbol.base_name)+
+      cpp_scopes.current_scope().suffix;
+    symbol.type.set(ID_tag, cpp_scopes.current_scope().prefix+id2string(symbol.base_name));
 
     // move early, must be visible before doing body
     symbolt *new_symbol;
@@ -262,10 +266,11 @@ void cpp_typecheckt::typecheck_compound_type(
     id.id_class=cpp_idt::CLASS;
     id.is_scope=true;
     id.prefix=cpp_scopes.current_scope().prefix+
-              id2string(new_symbol->base_name)+"::";
+              id2string(new_symbol->base_name)+
+              cpp_scopes.current_scope().suffix+"::";
     id.class_identifier=new_symbol->name;
     id.id_class=cpp_idt::CLASS;
-
+    
     if(has_body)
       typecheck_compound_body(*new_symbol);
     else