CBMC: symbol_table_buildert Class Reference

CBMC

Loading...

Searching...

No Matches

Public Member Functions | Static Public Member Functions | Private Attributes | List of all members

symbol_table_buildert Class Reference

Author: Diffblue Ltd. More...

#include <symbol_table_builder.h>

+ Inheritance diagram for symbol_table_buildert:

+ Collaboration diagram for symbol_table_buildert:

Public Member Functions

symbol_table_buildert (symbol_table_baset &base_symbol_table)

symbol_table_buildert (symbol_table_buildert &&other)

symbol_table_buildert (const symbol_table_buildert &)=delete

symbol_table_buildert & operator= (const symbol_table_buildert &)=delete

symbol_table_buildert & operator= (symbol_table_buildert &&)=delete

const symbol_tablet & get_symbol_table () const override

void erase (const symbolst::const_iterator &entry) override

Remove a symbol from the symbol table.

void clear () override

bool move (symbolt &symbol, symbolt *&new_symbol) override

symbolt * get_writeable (const irep_idt &identifier) override

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

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

Move or copy a new symbol to the symbol table.

iteratort begin () override

iteratort end () override

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

std::size_t next_unused_suffix (const std::string &prefix) const override

Try to find the next free identity for the passed-in prefix in this symbol table.

virtual iteratort begin ()=0

virtual const_iteratort begin () const

virtual iteratort end ()=0

virtual const_iteratort end () const

- 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_baset & operator= (const symbol_table_baset &other)=delete

virtual ~symbol_table_baset ()

Author: Diffblue Ltd.

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.

operator const symbol_tablet & () const

Permits implicit cast to const symbol_tablet &.

bool has_symbol (const irep_idt &name) const

Check whether a symbol exists in the symbol table.

const symbolt * lookup (const irep_idt &name) const

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

const symbolt & lookup_ref (const irep_idt &name) const

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

std::list< symbolst::const_iterator > match_name_or_base_name (const irep_idt &id) const

Collect all symbols the name of which matches id or the base name of which matches id.

symbolt & get_writeable_ref (const irep_idt &name)

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

bool add (const symbolt &symbol)

Add a new symbol to the symbol table.

bool remove (const irep_idt &name)

Remove a symbol from the symbol table.

void show (std::ostream &out) const

Print the contents of the symbol table.

std::vector< irep_idt > sorted_symbol_names () const

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

Static Public Member Functions

static symbol_table_buildert wrap (symbol_table_baset &base_symbol_table)

Private Attributes

symbol_table_baset & base_symbol_table

std::map< std::string, std::size_t > next_free_suffix_for_prefix

Additional Inherited Members

- Public Types inherited from symbol_table_baset

typedef std::unordered_map< irep_idt, symbolt > symbolst

using const_iteratort = symbolst::const_iterator

- Public Attributes inherited from symbol_table_baset

const symbolst & symbols

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

const symbol_base_mapt & symbol_base_map

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

const symbol_module_mapt & symbol_module_map

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

Detailed Description

Author: Diffblue Ltd.

Wrapper around a symbol table that keeps track of suffixes for faster calculation of the smallest unused suffix.

Definition at line 13 of file symbol_table_builder.h.

Constructor & Destructor Documentation

◆ symbol_table_buildert() [1/3]

symbol_table_buildert::symbol_table_buildert ( symbol_table_baset & base_symbol_table )

inlineexplicit

Definition at line 20 of file symbol_table_builder.h.

◆ symbol_table_buildert() [2/3]

symbol_table_buildert::symbol_table_buildert ( symbol_table_buildert && other )

inline

Definition at line 29 of file symbol_table_builder.h.

◆ symbol_table_buildert() [3/3]

symbol_table_buildert::symbol_table_buildert ( const symbol_table_buildert & )

delete

Member Function Documentation

◆ begin() [1/3]

symbol_table_baset::const_iteratort symbol_table_baset::begin ( ) const

virtual

Reimplemented from symbol_table_baset.

Definition at line 273 of file symbol_table_base.cpp.

◆ begin() [2/3]

iteratort symbol_table_buildert::begin ( )

inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 78 of file symbol_table_builder.h.

◆ begin() [3/3]

virtual iteratort symbol_table_baset::begin ( )

virtual

Implements symbol_table_baset.

◆ clear()

void symbol_table_buildert::clear ( )

inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 57 of file symbol_table_builder.h.

◆ end() [1/3]

symbol_table_baset::const_iteratort symbol_table_baset::end ( ) const

virtual

Reimplemented from symbol_table_baset.

Definition at line 274 of file symbol_table_base.cpp.

◆ end() [2/3]

iteratort symbol_table_buildert::end ( )

inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 83 of file symbol_table_builder.h.

◆ end() [3/3]

virtual iteratort symbol_table_baset::end ( )

virtual

Implements symbol_table_baset.

◆ erase()

void symbol_table_buildert::erase ( const symbolst::const_iterator & entry )

inlineoverridevirtual

Remove a symbol from the symbol table.

Parameters: entry an iterator pointing at the symbol to remove

Implements symbol_table_baset.

Definition at line 52 of file symbol_table_builder.h.

◆ get_symbol_table()

const symbol_tablet & symbol_table_buildert::get_symbol_table ( ) const

inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 47 of file symbol_table_builder.h.

◆ get_writeable()

symbolt * symbol_table_buildert::get_writeable ( const irep_idt & name )

inlineoverridevirtual

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

Parameters: name The 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 68 of file symbol_table_builder.h.

◆ insert()

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

inlineoverridevirtual

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: symbol The 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 73 of file symbol_table_builder.h.

◆ move()

bool symbol_table_buildert::move ( symbolt & symbol,

symbolt *& new_symbol

)

inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 63 of file symbol_table_builder.h.

◆ next_unused_suffix()

std::size_t symbol_table_buildert::next_unused_suffix ( const std::string & prefix ) const

inlineoverridevirtual

Try to find the next free identity for the passed-in prefix in this symbol table.

Remarks: This method needs to generate names deterministically in regards to operations that generate the same prefix (and any other operation shouldn't affect this).

Due to this requirement we don't do anything fancy in regards to attempting to find the absolute earliest free suffix if one has been deleted, only the next free increment from our last stored value.

Reimplemented from symbol_table_baset.

Definition at line 107 of file symbol_table_builder.h.

◆ operator=() [1/2]

symbol_table_buildert & symbol_table_buildert::operator= ( const symbol_table_buildert & )

delete

◆ operator=() [2/2]

symbol_table_buildert & symbol_table_buildert::operator= ( symbol_table_buildert && )

delete

◆ validate()

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

inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 91 of file symbol_table_builder.h.

◆ wrap()

static symbol_table_buildert symbol_table_buildert::wrap ( symbol_table_baset & base_symbol_table )

inlinestatic

Definition at line 42 of file symbol_table_builder.h.

Member Data Documentation

◆ base_symbol_table

symbol_table_baset& symbol_table_buildert::base_symbol_table

private

Definition at line 16 of file symbol_table_builder.h.

◆ next_free_suffix_for_prefix

std::map<std::string, std::size_t> symbol_table_buildert::next_free_suffix_for_prefix

mutableprivate

Definition at line 17 of file symbol_table_builder.h.

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

/home/runner/work/cbmc/cbmc/src/util/symbol_table_builder.h

symbol_table_buildert
Generated by doxygen 1.9.8