Snapshot of the symbolic data needed to merge a deferred path. More...

#include <goto_symex_state.h>

Public Member Functions
	merge_statet (const goto_symex_statet &s)
	merge_statet (const merge_statet &s)
merge_statet &	operator= (const merge_statet &)
	~merge_statet ()=default

Public Attributes
unsigned	num_instructions
std::shared_ptr< renaming::level2t >	level2_ptr
renaming::level2t &	level2
value_sett	value_set
guard2tc	guard
unsigned int	thread_id
renaming::level1t::current_namest	level1_names
variable_name_sett	local_variables
std::shared_ptr< void >	interval_snapshot
BigInt	stack_frame_total

Detailed Description

Snapshot of the symbolic data needed to merge a deferred path.

merge_statet is intentionally smaller than goto_symex_statet. It is used for GOTO/function-return/function-pointer paths that will be joined at a later instruction, so it only keeps the data the merge operation reads: the SSA renaming state, value set, guard, instruction depth, thread id, and current frame's L1 renaming and local-variable set.

It deliberately does not carry the full thread execution state, such as the program counter, source location, call stack, loop counters, exception state, or global guard.

Constructor & Destructor Documentation

◆ merge_statet() [1/2]

goto_symex_statet::merge_statet::merge_statet ( const goto_symex_statet & s )

inlineexplicit

◆ merge_statet() [2/2]

goto_symex_statet::merge_statet::merge_statet ( const merge_statet & s )

inlineexplicit

◆ ~merge_statet()

goto_symex_statet::merge_statet::~merge_statet ( )

default

Member Function Documentation

◆ operator=()

merge_statet & goto_symex_statet::merge_statet::operator= ( const merge_statet & )

inline

Member Data Documentation

◆ guard

guard2tc goto_symex_statet::merge_statet::guard

◆ interval_snapshot

std::shared_ptr<void> goto_symex_statet::merge_statet::interval_snapshot

◆ level1_names

renaming::level1t::current_namest goto_symex_statet::merge_statet::level1_names

◆ level2

renaming::level2t& goto_symex_statet::merge_statet::level2

◆ level2_ptr

std::shared_ptr<renaming::level2t> goto_symex_statet::merge_statet::level2_ptr

◆ local_variables

variable_name_sett goto_symex_statet::merge_statet::local_variables

◆ num_instructions

unsigned goto_symex_statet::merge_statet::num_instructions

◆ stack_frame_total

BigInt goto_symex_statet::merge_statet::stack_frame_total

◆ thread_id

unsigned int goto_symex_statet::merge_statet::thread_id

◆ value_set

value_sett goto_symex_statet::merge_statet::value_set

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

src/goto-symex/state/goto_symex_state.h

Public Member Functions

Public Attributes