replace_symbolt Class Reference

Replace a symbol expression by a given expression. More...

#include <replace_symbol.h>

Inheritance diagram for replace_symbolt:

Collaboration diagram for replace_symbolt:

Public Types
typedef std::unordered_map< irep_idt, exprt >	expr_mapt

Public Member Functions
void	insert (const class symbol_exprt &old_expr, const exprt &new_expr)
	Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothing (i.e. More...
void	set (const class symbol_exprt &old_expr, const exprt &new_expr)
	Sets old_expr to be replaced by new_expr. More...
virtual bool	replace (exprt &dest) const
virtual bool	replace (typet &dest) const
void	operator() (exprt &dest) const
void	operator() (typet &dest) const
void	clear ()
bool	empty () const
std::size_t	erase (const irep_idt &id)
expr_mapt::iterator	erase (expr_mapt::iterator it)
bool	replaces_symbol (const irep_idt &id) const
	replace_symbolt ()
virtual	~replace_symbolt ()
const expr_mapt &	get_expr_map () const
expr_mapt &	get_expr_map ()

Protected Member Functions
virtual bool	replace_symbol_expr (symbol_exprt &dest) const
bool	have_to_replace (const exprt &dest) const
bool	have_to_replace (const typet &type) const

Protected Attributes
expr_mapt	expr_map
std::set< irep_idt >	bindings

Detailed Description

Replace a symbol expression by a given expression.

The type of the symbol must match the type of the replacement. This class is aware of symbol hiding caused by bindings such as forall, exists, and the like.

Definition at line 27 of file replace_symbol.h.

Member Typedef Documentation

expr_mapt

typedef std::unordered_map<irep_idt, exprt> replace_symbolt::expr_mapt

Definition at line 30 of file replace_symbol.h.

Constructor & Destructor Documentation

replace_symbolt()

replace_symbolt::replace_symbolt

(

)

Definition at line 16 of file replace_symbol.cpp.

~replace_symbolt()

replace_symbolt::~replace_symbolt ( )

virtual

Definition at line 20 of file replace_symbol.cpp.

Member Function Documentation

clear()

void replace_symbolt::clear ( void  )

inline

Definition at line 54 of file replace_symbol.h.

empty()

bool replace_symbolt::empty ( ) const

inline

Definition at line 59 of file replace_symbol.h.

erase() [1/2]

std::size_t replace_symbolt::erase ( const irep_idt &  id )

inline

Definition at line 64 of file replace_symbol.h.

erase() [2/2]

expr_mapt::iterator replace_symbolt::erase ( expr_mapt::iterator  it )

inline

Definition at line 69 of file replace_symbol.h.

get_expr_map() [1/2]

expr_mapt& replace_symbolt::get_expr_map ( )

inline

Definition at line 87 of file replace_symbol.h.

get_expr_map() [2/2]

const expr_mapt& replace_symbolt::get_expr_map ( ) const

inline

Definition at line 82 of file replace_symbol.h.

have_to_replace() [1/2]

bool replace_symbolt::have_to_replace ( const exprt &  dest ) const

protected

Definition at line 164 of file replace_symbol.cpp.

have_to_replace() [2/2]

bool replace_symbolt::have_to_replace ( const typet &  type ) const

protected

Definition at line 272 of file replace_symbol.cpp.

insert()

void replace_symbolt::insert	(	const class symbol_exprt &	old_expr,
		const exprt &	new_expr
	)

Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothing (i.e.

std::map::insert-like behaviour).

Definition at line 24 of file replace_symbol.cpp.

operator()() [1/2]

void replace_symbolt::operator() ( exprt &  dest ) const

inline

Definition at line 44 of file replace_symbol.h.

operator()() [2/2]

void replace_symbolt::operator() ( typet &  dest ) const

inline

Definition at line 49 of file replace_symbol.h.

replace() [1/2]

bool replace_symbolt::replace ( exprt &  dest ) const

virtual

Reimplemented in address_of_aware_replace_symbolt, and casting_replace_symbolt.

Definition at line 64 of file replace_symbol.cpp.

replace() [2/2]

bool replace_symbolt::replace ( typet &  dest ) const

virtual

Definition at line 206 of file replace_symbol.cpp.

replace_symbol_expr()

bool replace_symbolt::replace_symbol_expr ( symbol_exprt &  dest ) const

protectedvirtual

Reimplemented in address_of_aware_replace_symbolt, unchecked_replace_symbolt, and casting_replace_symbolt.

Definition at line 43 of file replace_symbol.cpp.

replaces_symbol()

bool replace_symbolt::replaces_symbol ( const irep_idt &  id ) const

inline

Definition at line 74 of file replace_symbol.h.

set()

void replace_symbolt::set	(	const class symbol_exprt &	old_expr,
		const exprt &	new_expr
	)

Sets old_expr to be replaced by new_expr.

Definition at line 36 of file replace_symbol.cpp.

Member Data Documentation

bindings

std::set<irep_idt> replace_symbolt::bindings

mutableprotected

Definition at line 94 of file replace_symbol.h.

expr_map

expr_mapt replace_symbolt::expr_map

protected

Definition at line 93 of file replace_symbol.h.

---

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

• /home/runner/work/cbmc/cbmc/src/util/replace_symbol.h
• /home/runner/work/cbmc/cbmc/src/util/replace_symbol.cpp