execution_statet::state_hashing_level2t Class Reference

State-hashing level2t. More...

#include <execution_state.h>

Inheritance diagram for execution_statet::state_hashing_level2t:

Public Types
typedef std::map< irep_idt, std::size_t >	current_state_hashest
Public Types inherited from renaming::level2t
typedef persistent_map< name_record, valuet, name_rec_hash >	current_namest

Public Member Functions
	state_hashing_level2t (execution_statet &ref)
	~state_hashing_level2t () override=default
std::shared_ptr< renaming::level2t >	clone () const override
void	make_assignment (expr2tc &lhs_symbol, const expr2tc &const_value, const expr2tc &assigned_value) override
std::size_t	generate_l2_state_hash () const
Public Member Functions inherited from execution_statet::ex_state_level2t
	ex_state_level2t (execution_statet &ref)
	~ex_state_level2t () override=default
void	rename (expr2tc &lhs_symbol, unsigned count) override
void	rename (expr2tc &identifier) override
Public Member Functions inherited from renaming::level2t
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
current_state_hashest	current_hashes
Public Attributes inherited from execution_statet::ex_state_level2t
execution_statet *	owner
Public Attributes inherited from renaming::level2t
current_namest	current_names

Additional Inherited Members
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

State-hashing level2t.

When using this level2t, any assignment made is caught, and the symbolic names are hashed. This is the primary handler for state hashing.

Member Typedef Documentation

current_state_hashest

typedef std::map<irep_idt, std::size_t> execution_statet::state_hashing_level2t::current_state_hashest

Constructor & Destructor Documentation

state_hashing_level2t()

execution_statet::state_hashing_level2t::state_hashing_level2t

(

execution_statet &

ref

)

~state_hashing_level2t()

execution_statet::state_hashing_level2t::~state_hashing_level2t ( )

overridedefault

Member Function Documentation

clone()

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

overridevirtual

Reimplemented from execution_statet::ex_state_level2t.

generate_l2_state_hash()

std::size_t execution_statet::state_hashing_level2t::generate_l2_state_hash

(

)

const

make_assignment()

void execution_statet::state_hashing_level2t::make_assignment ( expr2tc & lhs_symbol, const expr2tc & const_value, const expr2tc & assigned_value )

overridevirtual

Reimplemented from renaming::level2t.

Member Data Documentation

current_hashes

current_state_hashest execution_statet::state_hashing_level2t::current_hashes

---

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