namespace.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Namespace
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#include "namespace.h"
 
#include <algorithm>
 
#include "c_types.h"
#include "std_expr.h"
#include "symbol_table.h"
 
namespace_baset::~namespace_baset()
{
}
 
const symbolt &namespace_baset::lookup(const symbol_exprt &expr) const
{
  return lookup(expr.get_identifier());
}
 
const symbolt &namespace_baset::lookup(const tag_typet &type) const
{
  return lookup(type.get_identifier());
}
 
const typet &namespace_baset::follow(const typet &src) const
{
  if(src.id() == ID_union_tag)
    return follow_tag(to_union_tag_type(src));
 
  if(src.id() == ID_struct_tag)
    return follow_tag(to_struct_tag_type(src));
 
  return src;
}
 
const union_typet &namespace_baset::follow_tag(const union_tag_typet &src) const
{
  const symbolt &symbol=lookup(src.get_identifier());
  CHECK_RETURN(symbol.is_type);
  CHECK_RETURN(symbol.type.id() == ID_union);
  return to_union_type(symbol.type);
}
 
const struct_typet &
namespace_baset::follow_tag(const struct_tag_typet &src) const
{
  const symbolt &symbol=lookup(src.get_identifier());
  CHECK_RETURN(symbol.is_type);
  CHECK_RETURN(symbol.type.id() == ID_struct);
  return to_struct_type(symbol.type);
}
 
const c_enum_typet &
namespace_baset::follow_tag(const c_enum_tag_typet &src) const
{
  const symbolt &symbol=lookup(src.get_identifier());
  CHECK_RETURN(symbol.is_type);
  CHECK_RETURN(symbol.type.id() == ID_c_enum);
  return to_c_enum_type(symbol.type);
}
 
void namespace_baset::follow_macros(exprt &expr) const
{
  if(expr.id()==ID_symbol)
  {
    const symbolt &symbol = lookup(to_symbol_expr(expr));
 
    if(symbol.is_macro && !symbol.value.is_nil())
    {
      expr=symbol.value;
      follow_macros(expr);
    }
 
    return;
  }
 
  Forall_operands(it, expr)
    follow_macros(*it);
}
 
std::size_t namespacet::smallest_unused_suffix(const std::string &prefix) const
{
  std::size_t m = 0;
 
  if(symbol_table1!=nullptr)
    m = std::max(m, symbol_table1->next_unused_suffix(prefix));
 
  if(symbol_table2!=nullptr)
    m = std::max(m, symbol_table2->next_unused_suffix(prefix));
 
  return m;
}
 
bool namespacet::lookup(
  const irep_idt &name,
  const symbolt *&symbol) const
{
  symbol_tablet::symbolst::const_iterator it;
 
  if(symbol_table1!=nullptr)
  {
    it=symbol_table1->symbols.find(name);
 
    if(it!=symbol_table1->symbols.end())
    {
      symbol=&(it->second);
      return false;
    }
  }
 
  if(symbol_table2!=nullptr)
  {
    it=symbol_table2->symbols.find(name);
 
    if(it!=symbol_table2->symbols.end())
    {
      symbol=&(it->second);
      return false;
    }
  }
 
  return true;
}
 
std::size_t
multi_namespacet::smallest_unused_suffix(const std::string &prefix) const
{
  std::size_t m = 0;
 
  for(const auto &st : symbol_table_list)
    m = std::max(m, st->next_unused_suffix(prefix));
 
  return m;
}
 
bool multi_namespacet::lookup(
  const irep_idt &name,
  const symbolt *&symbol) const
{
  symbol_tablet::symbolst::const_iterator s_it;
 
  for(symbol_table_listt::const_iterator
      c_it=symbol_table_list.begin();
      c_it!=symbol_table_list.end();
      c_it++)
  {
    s_it=(*c_it)->symbols.find(name);
 
    if(s_it!=(*c_it)->symbols.end())
    {
      symbol=&(s_it->second);
      return false;
    }
  }
 
  return true;
}