cprover
namespacet Class Reference

A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in them. More...

#include <namespace.h>

+ Inheritance diagram for namespacet:
+ Collaboration diagram for namespacet:

Public Member Functions

 namespacet (const symbol_tablet &_symbol_table)
 
 namespacet (const symbol_tablet &_symbol_table1, const symbol_tablet &_symbol_table2)
 
 namespacet (const symbol_tablet *_symbol_table1, const symbol_tablet *_symbol_table2)
 
bool lookup (const irep_idt &name, const symbolt *&symbol) const override
 See documentation for namespace_baset::lookup(). More...
 
std::size_t smallest_unused_suffix (const std::string &prefix) const override
 See documentation for namespace_baset::smallest_unused_suffix(). More...
 
const symbol_tabletget_symbol_table () const
 Return first symbol table registered with the namespace. More...
 
const symboltlookup (const irep_idt &name) const
 Lookup a symbol in the namespace. More...
 
const symboltlookup (const symbol_exprt &) const
 Generic lookup function for a symbol expression in a symbol table. More...
 
const symboltlookup (const symbol_typet &) const
 Generic lookup function for a symbol type in a symbol table. More...
 
const symboltlookup (const tag_typet &) const
 Generic lookup function for a tag type in a symbol table. More...
 
virtual bool lookup (const irep_idt &name, const symbolt *&symbol) const=0
 Searches for a symbol named name. More...
 
- Public Member Functions inherited from namespace_baset
const symboltlookup (const irep_idt &name) const
 Lookup a symbol in the namespace. More...
 
const symboltlookup (const symbol_exprt &) const
 Generic lookup function for a symbol expression in a symbol table. More...
 
const symboltlookup (const symbol_typet &) const
 Generic lookup function for a symbol type in a symbol table. More...
 
const symboltlookup (const tag_typet &) const
 Generic lookup function for a tag type in a symbol table. More...
 
virtual ~namespace_baset ()
 
void follow_macros (exprt &) const
 Follow macros to their values in a given expression. More...
 
const typetfollow (const typet &) const
 Resolve type symbol to the type it points to. More...
 
const typetfollow_tag (const union_tag_typet &) const
 Follow type tag of union type. More...
 
const typetfollow_tag (const struct_tag_typet &) const
 Follow type tag of struct type. More...
 
const typetfollow_tag (const c_enum_tag_typet &) const
 Follow type tag of enum type. More...
 

Protected Attributes

const symbol_tabletsymbol_table1
 
const symbol_tabletsymbol_table2
 

Detailed Description

A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in them.

The basic idea is that you might want to combine a value table and a type table, so that for a variable you can lookup both of these essential properties, in one structure.

Definition at line 92 of file namespace.h.

Constructor & Destructor Documentation

◆ namespacet() [1/3]

namespacet::namespacet ( const symbol_tablet _symbol_table)
inlineexplicit

Definition at line 96 of file namespace.h.

◆ namespacet() [2/3]

namespacet::namespacet ( const symbol_tablet _symbol_table1,
const symbol_tablet _symbol_table2 
)
inline

Definition at line 99 of file namespace.h.

◆ namespacet() [3/3]

namespacet::namespacet ( const symbol_tablet _symbol_table1,
const symbol_tablet _symbol_table2 
)
inline

Definition at line 107 of file namespace.h.

Member Function Documentation

◆ get_symbol_table()

const symbol_tablet& namespacet::get_symbol_table ( ) const
inline

Return first symbol table registered with the namespace.

Definition at line 125 of file namespace.h.

◆ lookup() [1/6]

const symbolt& namespace_baset::lookup
inline

Lookup a symbol in the namespace.

Parameters
nameThe name of the symbol to lookup.
Returns
: A reference to the symbol found.
Remarks
: It is a PRECONDITION that the symbol name exists in the namespace.

Definition at line 44 of file namespace.h.

◆ lookup() [2/6]

const symbolt & namespace_baset::lookup

Generic lookup function for a tag type in a symbol table.

Parameters
typeThe tag type to lookup.
Returns
The symbol found in the namespace.
Remarks
The lookup function called assumes that the tag symbol we are looking for exists in the symbol table. If it doesn't, it hits an INVARIANT.

Definition at line 72 of file namespace.cpp.

◆ lookup() [3/6]

virtual bool namespace_baset::lookup

Searches for a symbol named name.

Iff found, set symbol to point to the symbol and return false; else symbol is unmodified and true is returned. With multiple symbol tables, symbol_table1 is searched first and then symbol_table2.

Returns
False iff the requested symbol is found in at least one of the tables.

◆ lookup() [4/6]

const symbolt & namespace_baset::lookup

Generic lookup function for a symbol expression in a symbol table.

Parameters
exprThe symbol expression to lookup.
Returns
The symbol found in the namespace.
Remarks
The lookup function called assumes that the symbol we are looking for exists in the symbol table. If it doesn't, it hits an INVARIANT.

Definition at line 50 of file namespace.cpp.

◆ lookup() [5/6]

const symbolt & namespace_baset::lookup

Generic lookup function for a symbol type in a symbol table.

Parameters
typeThe symbol type to lookup.
Returns
The symbol found in the namespace.
Remarks
The lookup function called assumes that the type symbol we are looking for exists in the symbol table. If it doesn't, it hits an INVARIANT.

Definition at line 61 of file namespace.cpp.

◆ lookup() [6/6]

bool namespacet::lookup ( const irep_idt name,
const symbolt *&  symbol 
) const
overridevirtual

See documentation for namespace_baset::lookup().

Search for a given symbol by name, in the two symbol tables, if present.

Note that namespacet has two symbol tables.

Parameters
nameThe name of the symbol to be looked up.
symbolThe const pointer to the reference of the symbol if it's found during lookup.
Returns
False if the symbol was found, True otherwise.

Implements namespace_baset.

Reimplemented in multi_namespacet.

Definition at line 184 of file namespace.cpp.

◆ smallest_unused_suffix()

std::size_t namespacet::smallest_unused_suffix ( const std::string &  prefix) const
overridevirtual

See documentation for namespace_baset::smallest_unused_suffix().

Find smallest unused suffix in the two symbol tables, assuming they are present.

Parameters
prefixThe prefix to find smallest unused suffix of.
Returns
The smallest prefix size.

Implements namespace_baset.

Reimplemented in multi_namespacet.

Definition at line 166 of file namespace.cpp.

Member Data Documentation

◆ symbol_table1

const symbol_tablet* namespacet::symbol_table1
protected

Definition at line 131 of file namespace.h.

◆ symbol_table2

const symbol_tablet * namespacet::symbol_table2
protected

Definition at line 131 of file namespace.h.


The documentation for this class was generated from the following files: