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. More...

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. More...

std::pair< symbolt &, bool >	insert (symbolt symbol) override
	Move or copy a new symbol to the symbol table. More...

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. More...

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. 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...

	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 symbolt *	lookup (const irep_idt &name) const
	Find a symbol in the symbol table for read-only access. More...

const symbolt &	lookup_ref (const irep_idt &name) const
	Find a symbol in the symbol table for read-only access. More...

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`. More...

symbolt &	get_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...

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. More...

virtual const_iteratort	begin () const

virtual const_iteratort	end () const

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. More...

const symbol_base_mapt &	symbol_base_map
	Read-only field, used to look up symbol names given their base names. More...

const symbol_module_mapt &	symbol_module_map
	Read-only field, used to look up symbol names given their modules. More...

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

virtual

Implements 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 ( void )

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

virtual

Implements 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

Public Member Functions

Static Public Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ symbol_table_buildert() [1/3]

◆ symbol_table_buildert() [2/3]

◆ symbol_table_buildert() [3/3]

Member Function Documentation

◆ begin() [1/3]

◆ begin() [2/3]

◆ begin() [3/3]

◆ clear()

◆ end() [1/3]

◆ end() [2/3]

◆ end() [3/3]

◆ erase()

◆ get_symbol_table()

◆ get_writeable()

◆ insert()

◆ move()

◆ next_unused_suffix()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ validate()

◆ wrap()

Member Data Documentation

◆ base_symbol_table

◆ next_free_suffix_for_prefix