execution_statet::ex_state_level2t Class Reference

execution_statet specific level2t. More...

#include <execution_state.h>

Inheritance diagram for execution_statet::ex_state_level2t:

Public Member Functions
	ex_state_level2t (execution_statet &ref)
	~ex_state_level2t () override=default
std::shared_ptr< renaming::level2t >	clone () const override
void	rename (expr2tc &lhs_symbol, unsigned count) override
void	rename (expr2tc &identifier) override
Public Member Functions inherited from renaming::level2t
virtual void	make_assignment (expr2tc &lhs_symbol, const expr2tc &constant_value, const expr2tc &assigned_value)
void	rename (expr2tc &expr) override
void	get_ident_name (expr2tc &symbol) const override
void	remove (const expr2tc &symbol) override
valuet	current_value (const name_record &rec) const
	Get-or-default then re-store: the persistent map hands out immutable values, so a "modify the entry in place" site reads a copy, mutates it, and sets it back.
void	retire (const name_record &rec)
	Retire a name whose storage has gone out of scope.
void	declare (const name_record &rec)
	Record rec at its initial version.
void	get_original_name (expr2tc &expr) const override
void	set_constant (const name_record &rec, const expr2tc &value)
	Complete an assignment make_assignment has just made, whose value only its caller can build: #7597 re-offers a refused member write as a read of the L2 name make_assignment mints.
unsigned	current_number (const expr2tc &sym) const
unsigned	current_number (const name_record &rec) const
	level2t ()=default
	~level2t () override=default
virtual void	print (std::ostream &out) const
virtual void	dump () const
Public Member Functions inherited from renaming::renaming_levelt
virtual	~renaming_levelt ()=default

Public Attributes
execution_statet *	owner
Public Attributes inherited from renaming::level2t
current_namest	current_names

Additional Inherited Members
Public Types inherited from renaming::level2t
typedef persistent_map< name_record, valuet, name_rec_hash >	current_namest
Static Public Member Functions inherited from renaming::level2t
static void	rename_to_record (expr2tc &sym, const name_record &rec)
Static Public Member Functions inherited from renaming::renaming_levelt
static void	get_original_name (expr2tc &expr, symbol2t::renaming_level lev)
Protected Member Functions inherited from renaming::level2t
virtual void	coveredinbees (expr2tc &lhs_sym, unsigned count, unsigned node_id)

Detailed Description

execution_statet specific level2t.

The feature of this class is that we maintain a pointer to the ex_state that owns this level2t, which is updated whenever this class gets copied. We also override some level2t methods, so that we can encode a node_id in the names that are generated. (This is for –schedule).

Constructor & Destructor Documentation

ex_state_level2t()

execution_statet::ex_state_level2t::ex_state_level2t

(

execution_statet &

ref

)

~ex_state_level2t()

execution_statet::ex_state_level2t::~ex_state_level2t ( )

overridedefault

Member Function Documentation

clone()

std::shared_ptr< renaming::level2t > execution_statet::ex_state_level2t::clone ( ) const

overridevirtual

Implements renaming::level2t.

Reimplemented in execution_statet::state_hashing_level2t.

rename() [1/2]

void execution_statet::ex_state_level2t::rename ( expr2tc & identifier )

overridevirtual

Implements renaming::renaming_levelt.

rename() [2/2]

void execution_statet::ex_state_level2t::rename ( expr2tc & lhs_symbol, unsigned count )

overridevirtual

Implements renaming::level2t.

Member Data Documentation

owner

execution_statet* execution_statet::ex_state_level2t::owner

---

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

• src/goto-symex/scheduler/execution_state.h
• src/goto-symex/scheduler/execution_state.cpp