cprover
symbol_tablet Class Reference

The symbol table. More...

#include <symbol_table.h>

+ Inheritance diagram for symbol_tablet:
+ Collaboration diagram for symbol_tablet:

Public Member Functions

 symbol_tablet ()
 
 symbol_tablet (const symbol_tablet &other)
 Copy constructor. More...
 
symbol_tabletoperator= (const symbol_tablet &other)
 Copy assignment operator. More...
 
 symbol_tablet (symbol_tablet &&other)
 Move constructor. More...
 
symbol_tabletoperator= (symbol_tablet &&other)
 Move assignment operator. More...
 
void swap (symbol_tablet &other)
 Swap symbol maps between two symbol tables. More...
 
virtual const symbol_tabletget_symbol_table () const override
 
virtual symboltget_writeable (const irep_idt &name) override
 Find a symbol in the symbol table for read-write access. More...
 
virtual std::pair< symbolt &, bool > insert (symbolt symbol) override
 Author: Diffblue Ltd. More...
 
virtual bool move (symbolt &symbol, symbolt *&new_symbol) override
 Move a symbol into the symbol table. More...
 
virtual void erase (const symbolst::const_iterator &entry) override
 Remove a symbol from the symbol table. More...
 
virtual void clear () override
 Wipe internal state of the symbol table. More...
 
virtual iteratort begin () override
 
virtual iteratort end () override
 
void validate (const validation_modet vm=validation_modet::INVARIANT) const
 Check that the symbol table is well-formed. More...
 
- Public Member Functions inherited from symbol_table_baset
 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...
 
 operator const symbol_tablet & () const
 Permits implicit cast to const symbol_tablet &. More...
 
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...
 
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...
 
bool remove (const irep_idt &name)
 Remove a symbol from the symbol table. More...
 
void show (std::ostream &out) const
 Print the contents of the symbol table. More...
 

Private Attributes

symbolst internal_symbols
 
symbol_base_mapt internal_symbol_base_map
 
symbol_module_mapt internal_symbol_module_map
 

Additional Inherited Members

- Public Types inherited from symbol_table_baset
typedef std::unordered_map< irep_idt, symboltsymbolst
 
- Public Attributes inherited from symbol_table_baset
const symbolstsymbols
 
const symbol_base_maptsymbol_base_map
 
const symbol_module_maptsymbol_module_map
 

Detailed Description

The symbol table.

Definition at line 19 of file symbol_table.h.

Constructor & Destructor Documentation

◆ symbol_tablet() [1/3]

symbol_tablet::symbol_tablet ( )
inline

Definition at line 27 of file symbol_table.h.

◆ symbol_tablet() [2/3]

symbol_tablet::symbol_tablet ( const symbol_tablet other)
inline

Copy constructor.

Definition at line 36 of file symbol_table.h.

◆ symbol_tablet() [3/3]

symbol_tablet::symbol_tablet ( symbol_tablet &&  other)
inline

Move constructor.

Definition at line 55 of file symbol_table.h.

Member Function Documentation

◆ begin()

virtual iteratort symbol_tablet::begin ( )
inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 111 of file symbol_table.h.

◆ clear()

virtual void symbol_tablet::clear ( void  )
inlineoverridevirtual

Wipe internal state of the symbol table.

Implements symbol_table_baset.

Definition at line 104 of file symbol_table.h.

◆ end()

virtual iteratort symbol_tablet::end ( )
inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 115 of file symbol_table.h.

◆ erase()

void symbol_tablet::erase ( const symbolst::const_iterator &  entry)
overridevirtual

Remove a symbol from the symbol table.

Parameters
entryan iterator pointing at the symbol to remove

Implements symbol_table_baset.

Definition at line 86 of file symbol_table.cpp.

◆ get_symbol_table()

virtual const symbol_tablet& symbol_tablet::get_symbol_table ( ) const
inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 85 of file symbol_table.h.

◆ get_writeable()

virtual symbolt* symbol_tablet::get_writeable ( const irep_idt name)
inlineoverridevirtual

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.

Implements symbol_table_baset.

Definition at line 93 of file symbol_table.h.

◆ insert()

std::pair< symbolt &, bool > symbol_tablet::insert ( symbolt  symbol)
overridevirtual

Author: Diffblue Ltd.

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.

Implements symbol_table_baset.

Definition at line 17 of file symbol_table.cpp.

◆ move()

bool symbol_tablet::move ( symbolt symbol,
symbolt *&  new_symbol 
)
overridevirtual

Move a symbol into the symbol table.

If there is already a symbol with the same name then symbol is unchanged, new_symbol points to the symbol with the same name and true is returned. Otherwise, the symbol is moved into the symbol table, symbol is destroyed, new_symbol points to its new location in the symbol table and false is returned

Parameters
symbolThe symbol to be added to the symbol table
new_symbolPointer which the function will set to either point to the symbol in the symbol table with the same name or to the symbol that has been successfully moved into the symbol table
Returns
Returns a boolean indicating whether the process failed, which should only happen if there is a symbol with the same name already in the symbol table. If the process failed then symbol is unchanged and new_symbol points to the symbol with the same name. If the process succeeded symbol is set to be empty and new_symbol points to its new location in the symbol table

Implements symbol_table_baset.

Definition at line 63 of file symbol_table.cpp.

◆ operator=() [1/2]

symbol_tablet& symbol_tablet::operator= ( const symbol_tablet other)
inline

Copy assignment operator.

Definition at line 48 of file symbol_table.h.

◆ operator=() [2/2]

symbol_tablet& symbol_tablet::operator= ( symbol_tablet &&  other)
inline

Move assignment operator.

Definition at line 67 of file symbol_table.h.

◆ swap()

void symbol_tablet::swap ( symbol_tablet other)
inline

Swap symbol maps between two symbol tables.

Parameters
otherThe second symbol table to swap values with.

Definition at line 77 of file symbol_table.h.

◆ validate()

void symbol_tablet::validate ( const validation_modet  vm = validation_modet::INVARIANT) const

Check that the symbol table is well-formed.

Check whether the symbol table is in a valid state.

Parameters
vmDetermine whether to throw exceptions or trigger INVARIANT when validation fails.

Definition at line 123 of file symbol_table.cpp.

Member Data Documentation

◆ internal_symbol_base_map

symbol_base_mapt symbol_tablet::internal_symbol_base_map
private

Definition at line 23 of file symbol_table.h.

◆ internal_symbol_module_map

symbol_module_mapt symbol_tablet::internal_symbol_module_map
private

Definition at line 24 of file symbol_table.h.

◆ internal_symbols

symbolst symbol_tablet::internal_symbols
private

Definition at line 22 of file symbol_table.h.


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