namespace.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_UTIL_NAMESPACE_H
#define CPROVER_UTIL_NAMESPACE_H
 
#include "invariant.h"
#include "irep.h"
 
class exprt;
class symbolt;
class typet;
class symbol_exprt;
class tag_typet;
class union_typet;
class struct_typet;
class struct_union_typet;
class c_enum_typet;
class union_tag_typet;
class struct_tag_typet;
class struct_or_union_tag_typet;
class c_enum_tag_typet;
class symbol_table_baset;
 
class namespace_baset
{
public:
  // service methods
 
  const symbolt &lookup(const irep_idt &name) const
  {
    const symbolt *symbol;
    bool not_found = lookup(name, symbol);
    INVARIANT(
      !not_found,
      "we are assuming that a name exists in the namespace "
      "when this function is called - identifier " +
        id2string(name) + " was not found");
    return *symbol;
  }
 
  const symbolt &lookup(const symbol_exprt &) const;
  const symbolt &lookup(const tag_typet &) const;
 
  virtual ~namespace_baset();
 
  void follow_macros(exprt &) const;
 
  const union_typet &follow_tag(const union_tag_typet &) const;
  const struct_typet &follow_tag(const struct_tag_typet &) const;
  const c_enum_typet &follow_tag(const c_enum_tag_typet &) const;
  const struct_union_typet &follow_tag(const struct_or_union_tag_typet &) const;
 
  virtual std::size_t
  smallest_unused_suffix(const std::string &prefix) const = 0;
 
  virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const=0;
};
 
class namespacet:public namespace_baset
{
public:
  // constructors
  explicit namespacet(const symbol_table_baset &_symbol_table)
  { symbol_table1=&_symbol_table; symbol_table2=nullptr; }
 
  namespacet(
    const symbol_table_baset &_symbol_table1,
    const symbol_table_baset &_symbol_table2)
  {
    symbol_table1=&_symbol_table1;
    symbol_table2=&_symbol_table2;
  }
 
  namespacet(
    const symbol_table_baset *_symbol_table1,
    const symbol_table_baset *_symbol_table2)
  {
    symbol_table1=_symbol_table1;
    symbol_table2=_symbol_table2;
  }
 
  using namespace_baset::lookup;
 
  bool lookup(const irep_idt &name, const symbolt *&symbol) const override;
 
  std::size_t smallest_unused_suffix(const std::string &prefix) const override;
 
  const symbol_table_baset &get_symbol_table() const
  {
    return *symbol_table1;
  }
 
protected:
  const symbol_table_baset *symbol_table1, *symbol_table2;
};
 
class multi_namespacet:public namespacet
{
public:
  // constructors
  multi_namespacet():namespacet(nullptr, nullptr)
  {
  }
 
  explicit multi_namespacet(const symbol_table_baset &symbol_table)
    : namespacet(nullptr, nullptr)
  {
    add(symbol_table);
  }
 
  // these do the actual lookup
  using namespace_baset::lookup;
 
  bool lookup(const irep_idt &name, const symbolt *&symbol) const override;
  std::size_t smallest_unused_suffix(const std::string &prefix) const override;
 
  void add(const symbol_table_baset &symbol_table)
  {
    symbol_table_list.push_back(&symbol_table);
  }
 
protected:
  typedef std::vector<const symbol_table_baset *> symbol_table_listt;
  symbol_table_listt symbol_table_list;
};
 
#endif // CPROVER_UTIL_NAMESPACE_H