cprover
symbol_table_baset Class Referenceabstract

The symbol table base class interface. More...

#include <symbol_table_base.h>

+ Inheritance diagram for symbol_table_baset:
+ Collaboration diagram for symbol_table_baset:

Classes

class  iteratort
 

Public Types

typedef std::unordered_map< irep_idt, symboltsymbolst
 
using const_iteratort = symbolst::const_iterator
 

Public Member Functions

 symbol_table_baset (const symbolst &symbols, const symbol_base_mapt &symbol_base_map, const symbol_module_mapt &symbol_module_map)
 
 symbol_table_baset (const symbol_table_baset &other)=delete
 
symbol_table_basetoperator= (const symbol_table_baset &other)=delete
 
virtual ~symbol_table_baset ()
 Author: Diffblue Ltd. More...
 
std::size_t next_unused_suffix (const std::string &prefix, std::size_t start_number) const
 Find smallest unused integer i so that prefix + std::to_string(i) does not exist in the list symbols. More...
 
virtual std::size_t next_unused_suffix (const std::string &prefix) const
 
 operator const symbol_tablet & () const
 Permits implicit cast to const symbol_tablet &. More...
 
virtual const symbol_tabletget_symbol_table () const =0
 
bool has_symbol (const irep_idt &name) const
 Check whether a symbol exists in the symbol table. More...
 
const symboltlookup (const irep_idt &name) const
 Find a symbol in the symbol table for read-only access. More...
 
const symboltlookup_ref (const irep_idt &name) const
 Find a symbol in the symbol table for read-only access. More...
 
virtual symboltget_writeable (const irep_idt &name)=0
 Find a symbol in the symbol table for read-write access. More...
 
symboltget_writeable_ref (const irep_idt &name)
 Find a symbol in the symbol table for read-write access. More...
 
bool add (const symbolt &symbol)
 Add a new symbol to the symbol table. More...
 
virtual std::pair< symbolt &, bool > insert (symbolt symbol)=0
 Move or copy a new symbol to the symbol table. More...
 
virtual bool move (symbolt &symbol, symbolt *&new_symbol)=0
 
bool remove (const irep_idt &name)
 Remove a symbol from the symbol table. More...
 
virtual void erase (const symbolst::const_iterator &entry)=0
 Remove a symbol from the symbol table. More...
 
virtual void clear ()=0
 
void show (std::ostream &out) const
 Print the contents of the symbol table. More...
 
std::vector< irep_idtsorted_symbol_names () const
 Build and return a lexicographically sorted vector of symbol names from all symbols stored in this symbol table. More...
 
virtual iteratort begin ()=0
 
virtual iteratort end ()=0
 
virtual const_iteratort begin () const
 
virtual const_iteratort end () const
 

Public Attributes

const symbolstsymbols
 Read-only field, used to look up symbols given their names. More...
 
const symbol_base_maptsymbol_base_map
 Read-only field, used to look up symbol names given their base names. More...
 
const symbol_module_maptsymbol_module_map
 Read-only field, used to look up symbol names given their modules. More...
 

Detailed Description

The symbol table base class interface.

Definition at line 21 of file symbol_table_base.h.

Member Typedef Documentation

◆ const_iteratort

using symbol_table_baset::const_iteratort = symbolst::const_iterator

Definition at line 238 of file symbol_table_base.h.

◆ symbolst

typedef std::unordered_map<irep_idt, symbolt> symbol_table_baset::symbolst

Definition at line 24 of file symbol_table_base.h.

Constructor & Destructor Documentation

◆ symbol_table_baset() [1/2]

symbol_table_baset::symbol_table_baset ( const symbolst symbols,
const symbol_base_mapt symbol_base_map,
const symbol_module_mapt symbol_module_map 
)
inline

Definition at line 41 of file symbol_table_base.h.

◆ symbol_table_baset() [2/2]

symbol_table_baset::symbol_table_baset ( const symbol_table_baset other)
delete

◆ ~symbol_table_baset()

symbol_table_baset::~symbol_table_baset ( )
virtual

Author: Diffblue Ltd.

Destructor

Definition at line 9 of file symbol_table_base.cpp.

Member Function Documentation

◆ add()

bool symbol_table_baset::add ( const symbolt symbol)

Add a new symbol to the symbol table.

Parameters
symbolThe symbol to be added to the symbol table
Returns
Returns true if the process failed, which should only happen if there is a symbol with the same name already in the symbol table.

Definition at line 18 of file symbol_table_base.cpp.

◆ begin() [1/2]

symbol_table_baset::const_iteratort symbol_table_baset::begin ( ) const
virtual

Definition at line 68 of file symbol_table_base.cpp.

◆ begin() [2/2]

virtual iteratort symbol_table_baset::begin ( )
pure virtual

◆ clear()

virtual void symbol_table_baset::clear ( )
pure virtual

◆ end() [1/2]

symbol_table_baset::const_iteratort symbol_table_baset::end ( ) const
virtual

Definition at line 63 of file symbol_table_base.cpp.

◆ end() [2/2]

virtual iteratort symbol_table_baset::end ( )
pure virtual

◆ erase()

virtual void symbol_table_baset::erase ( const symbolst::const_iterator &  entry)
pure virtual

Remove a symbol from the symbol table.

Parameters
entryan iterator pointing at the symbol to remove

Implemented in symbol_tablet, symbol_table_buildert, and journalling_symbol_tablet.

◆ get_symbol_table()

virtual const symbol_tablet& symbol_table_baset::get_symbol_table ( ) const
pure virtual

◆ get_writeable()

virtual symbolt* symbol_table_baset::get_writeable ( const irep_idt name)
pure virtual

Find a symbol in the symbol table for read-write access.

Parameters
nameThe name of the symbol to look for
Returns
A pointer to the found symbol if it exists, nullptr otherwise.

Implemented in symbol_tablet, journalling_symbol_tablet, and symbol_table_buildert.

◆ get_writeable_ref()

symbolt& symbol_table_baset::get_writeable_ref ( const irep_idt name)
inline

Find a symbol in the symbol table for read-write access.

Parameters
nameThe name of the symbol to look for.
Returns
A reference to the symbol.
Exceptions
<tt>std::out_of_range</tt>if no such symbol exists

Definition at line 121 of file symbol_table_base.h.

◆ has_symbol()

bool symbol_table_baset::has_symbol ( const irep_idt name) const
inline

Check whether a symbol exists in the symbol table.

Parameters
nameThe name of the symbol to look for
Returns
True if the symbol exists

Definition at line 87 of file symbol_table_base.h.

◆ insert()

virtual std::pair<symbolt &, bool> symbol_table_baset::insert ( symbolt  symbol)
pure virtual

Move or copy a new symbol to the symbol table.

Remarks
: This is a nicer interface than move and achieves the same result as both move and add
Parameters
symbolThe symbol to be added to the symbol table - can be moved or copied in.
Returns
Returns a reference to the newly inserted symbol or to the existing symbol if a symbol with the same name already exists in the symbol table, along with a bool that is true if a new symbol was inserted.

Implemented in journalling_symbol_tablet, symbol_tablet, and symbol_table_buildert.

◆ lookup()

const symbolt* symbol_table_baset::lookup ( const irep_idt name) const
inline

Find a symbol in the symbol table for read-only access.

Parameters
nameThe name of the symbol to look for
Returns
A pointer to the found symbol if it exists, nullptr otherwise.

Definition at line 95 of file symbol_table_base.h.

◆ lookup_ref()

const symbolt& symbol_table_baset::lookup_ref ( const irep_idt name) const
inline

Find a symbol in the symbol table for read-only access.

Parameters
nameThe name of the symbol to look for
Returns
A reference to the symbol

Definition at line 104 of file symbol_table_base.h.

◆ move()

virtual bool symbol_table_baset::move ( symbolt symbol,
symbolt *&  new_symbol 
)
pure virtual

◆ next_unused_suffix() [1/2]

virtual std::size_t symbol_table_baset::next_unused_suffix ( const std::string &  prefix) const
inlinevirtual

Reimplemented in journalling_symbol_tablet, and symbol_table_buildert.

Definition at line 72 of file symbol_table_base.h.

◆ next_unused_suffix() [2/2]

std::size_t symbol_table_baset::next_unused_suffix ( const std::string &  prefix,
std::size_t  start_number 
) const
inline

Find smallest unused integer i so that prefix + std::to_string(i) does not exist in the list symbols.

Parameters
prefixA string denoting the prefix we want to find the smallest suffix of.
start_numberThe starting suffix number to search from.
Returns
The small unused suffix size.

Definition at line 63 of file symbol_table_base.h.

◆ operator const symbol_tablet &()

symbol_table_baset::operator const symbol_tablet & ( ) const
inline

Permits implicit cast to const symbol_tablet &.

Definition at line 78 of file symbol_table_base.h.

◆ operator=()

symbol_table_baset& symbol_table_baset::operator= ( const symbol_table_baset other)
delete

◆ remove()

bool symbol_table_baset::remove ( const irep_idt name)

Remove a symbol from the symbol table.

Parameters
nameThe name of the symbol to remove
Returns
Returns a boolean indicating whether the process failed i.e. false if the symbol was removed, or true if it didn't exist.

Definition at line 27 of file symbol_table_base.cpp.

◆ show()

void symbol_table_baset::show ( std::ostream &  out) const

Print the contents of the symbol table.

Parameters
outThe ostream to direct output to.

Definition at line 54 of file symbol_table_base.cpp.

◆ sorted_symbol_names()

std::vector< irep_idt > symbol_table_baset::sorted_symbol_names ( ) const

Build and return a lexicographically sorted vector of symbol names from all symbols stored in this symbol table.

Definition at line 36 of file symbol_table_base.cpp.

Member Data Documentation

◆ symbol_base_map

const symbol_base_mapt& symbol_table_baset::symbol_base_map

Read-only field, used to look up symbol names given their base names.

See symbols.

Definition at line 33 of file symbol_table_base.h.

◆ symbol_module_map

const symbol_module_mapt& symbol_table_baset::symbol_module_map

Read-only field, used to look up symbol names given their modules.

See symbols. Note that symbols whose module is empty are not recorded in this map. Currently only used in EBMC.

Definition at line 38 of file symbol_table_base.h.

◆ symbols

const symbolst& symbol_table_baset::symbols

Read-only field, used to look up symbols given their names.

Typically a subclass will have its own corresponding writeable field, and the read-only fields declared here function as "getters" for them.

Definition at line 30 of file symbol_table_base.h.


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