Class to explore states reachable through threading. More...

#include <reachability_tree.h>

Classes
struct	reduction_statst
	Why the schedule space shrank. More...
struct	scheduler_framet
struct	exploration_framet

Public Member Functions
	reachability_treet (goto_functionst &goto_functions, const namespacet &ns, optionst &opts, std::shared_ptr< symex_targett > target, contextt &context)
	Default constructor.
virtual	~reachability_treet ()=default
	Default destructor.
void	setup_for_new_explore ()
	Reinitialize for making new exploration of given functions.
execution_statet &	get_cur_state ()
	Return current execution_statet being explored / symex'd.
const execution_statet &	get_cur_state () const
bool	reset_to_unexplored_state ()
	Walks back to an unexplored context switch.
bool	has_more_states ()
	Are there more execution_statet s to explore.
int	get_CS_bound () const
	Permitted number of context switches to take.
int	get_ileave_direction_from_user () const
	Ask user for context switch to take.
bool	check_thread_viable (unsigned int tid, bool quiet) const
	Determine if a thread can be run.
void	mark_active_thread_explored ()
	Mark the active thread as already explored in the current scheduler frame.
bool	check_for_hash_collision () const
	Check whether current ex_state is a state hash collision.
void	post_hash_collision_cleanup ()
	Perform various pieces of accounting after a hash collision - primarily, ensuring that no further paths from this cswitch are explored.
void	update_hash_collision_set ()
	Update seen state hashes to contain current state.
void	remove_hash_collision_entry ()
	Remove the current state's hash from the seen set.
void	create_next_state ()
	Perform context switch operation triggered elsewhere.
bool	step_next_state ()
	Force a context switch, and take it.
unsigned int	decide_ileave_direction (execution_statet &ex_state)
	Pick a context switch to take.
void	print_ileave_trace () const
	Prints state of execution_statet stack.
bool	is_has_complete_formula ()
	Have we generated a full program trace.
void	go_next_state ()
	Advance to the next exploration frame, draining if we're at the top.
void	switch_to_next_execution_state ()
	Switch into just-generated execution state.
goto_symext::symex_resultt	get_next_formula ()
	Run threads to generate new trace.
goto_symext::symex_resultt	generate_schedule_formula ()
	Run threads in –schedule manner.
bool	setup_next_formula ()
	Reset ex_state stack to unexplored state.
void	report_reduction_stats () const
	Log the reduction counters.
void	mark_search_truncated ()
	Record that the subtree below the frame being explored was cut short – by the context bound, by MPOR, by a state-hash collision, by an unwind bound truncating a loop, or by __ESBMC_switch_away_from – rather than exhausted.
bool	is_address_taken_local (const irep_idt &name) const
bool	is_shared_storage (const symbolt &s) const
	Static or heap storage, or a local whose address may reach a thread.
bool	may_be_written (const irep_idt &name) const
	True if name may be written by some thread somewhere in the program.

Static Public Member Functions
static bool	has_shared_lifetime (const symbolt &s)
	Static or heap storage: shared however it is reached.

Public Attributes
goto_functionst &	goto_functions
	GOTO functions we're operating over.
contextt &	permanent_context
	Context we're operating upon.
bool	has_complete_formula
	Flag indicating we've executed all threads to exhaustion.
bool	state_hashing
	State hashing is enabled.
bool	directed_interleavings
	Functions dictate interleavings; perform no exploration.
const namespacet &	ns
	Namespace we're operating in.
optionst &	options
	Options that are enabled.
bool	cs_bound_pruned
	–context-bound cut an available switch: the schedule space was truncated rather than exhausted (issue #6480).
reduction_statst	reduction_stats

Protected Member Functions
scheduler_framet &	get_cur_scheduler_frame ()
const scheduler_framet &	get_cur_scheduler_frame () const
void	wake_dependent_sleepers ()
	Wake any sleeping thread the transition just taken is dependent on.
bool	dfs_explore_thread (unsigned int tid)
void	erase_current_frame ()
void	drain_to_unexplored (bool add_leak_checks)
	Drain fully-explored frames from the top of exploration_frames until step_next_state finds an unexplored switch (or the stack empties).
void	scan_program_writes ()
	Walk all goto instructions once and collect the names of every global that may be written.
void	scan_address_taken ()
	Fill address_taken_globals and address_taken_locals from every body.

Protected Attributes
std::list< exploration_framet >	exploration_frames
	Stack of exploration frames representing the current interleaving.
std::list< exploration_framet >::iterator	cur_frame_it
	Iterator recording the exploration frame we're operating on.
std::shared_ptr< symex_targett >	schedule_target
	"Global" symex target for output from –schedule exploration
std::shared_ptr< symex_targett >	target_template
	Target template; from which all targets are cloned.
int	CS_bound
	Limit on context switches; -1 for no limit.
int	TS_slice
	Timeslice limit read from the "time-slice" option; currently unused.
unsigned int	schedule_total_claims
	Number of claims in current –schedule exploration.
unsigned int	schedule_remaining_claims
	Number of remaining claims in current –schedule exploration.
unsigned int	schedule_simplified_claims
	Number of trivial claims in current –schedule exploration.
unsigned int	schedule_bounded_loop_truncations
	Loops cut off at the unwinding bound in current –schedule exploration.
unsigned int	next_thread_id
	Next thread ID to switch to, decided by analyse_* routines.
bool	por
	Whether partial-order-reduction is enabled.
bool	sleep_sets
	Whether sleep sets prune the search (–sleep-sets).
std::unordered_map< std::size_t, int >	hit_hashes
	State hashes discovered, mapped to the smallest context-switch count at which each was seen.
bool	interactive_ileaves
	Flag as to whether we're picking interleaving directions explicitly.
bool	schedule
	Are we using the –schedule scheduling method?
bool	smt_during_symex
	Are we using the –smt-during-symex method?
std::unordered_map< expr2tc, std::list< unsigned int >, irep2_hash >	vars_map
std::unordered_set< expr2tc, irep2_hash >	is_global
std::unordered_set< irep_idt, irep_id_hash >	ever_written_globals
	Static over-approximation of globals that may be written anywhere in the program.
std::unordered_set< irep_idt, irep_id_hash >	address_taken_globals
	Globals whose address is taken anywhere in the program (including the global initialisers in __ESBMC_main).
std::unordered_set< irep_idt, irep_id_hash >	address_taken_locals
	Non-static locals whose address is taken anywhere.
bool	any_indirect_write = false
	Set when the static scan sees a write through a pointer it cannot resolve.
bool	readonly_global_opt = false
	Master switch; wired to –cswitch-skip-readonly-globals.

Friends
class	execution_statet
void	build_goto_symex_classes ()

Detailed Description

Class to explore states reachable through threading.

Runs an execution_statet that explores code containing threading functions, and when notified of context-switch generating operations, attempts to interleave threads in all possible ways.

The primary piece of state is an ordered sequence of exploration_framet (a std::list, intentionally — we hand out iterators that must stay stable across pushes/erases elsewhere in the sequence), each pairing one execution_statet (the program state at a context-switch point) with a scheduler_framet that tracks which switches from that point have already been explored.

The algorithm is to run until the program completes and feed the trace to the caller. From then on, when asked to generate a new trace we:

Pop the final exploration frame.
Move to the new final frame on the stack.
Inspect whether we've explored all switches from this state. If yes, goto 1.
Pick a context switch to take from the current state and mark it explored on the frame's scheduler.
Push a fresh exploration frame: a clone of the execution state paired with a default scheduler_framet sized to the new thread count.
In the new top frame, switch to the chosen thread and continue symbolic execution from there. Fin.

There are various scheduling possibilities. The default is depth-first search, where we just follow the algorithm above and return all the traces to the caller. The "schedule" way combines all paths into one trace, which is then solved once.

Some kind of scheduling interface/api would be good for the future.

Constructor & Destructor Documentation

◆ reachability_treet()

reachability_treet::reachability_treet	(	goto_functionst &	goto_functions,
		const namespacet &	ns,
		optionst &	opts,
		std::shared_ptr< symex_targett >	target,
		contextt &	context )

Default constructor.

Requires a list of functions, and the namespace/context that we'll be working it, as well as the list of options to work with. The symex_targett pointer exists to allow the creator of this RT to feed a subclass of symex_targett into the RT, performing some additional actions than just collecting assignments/etc.

Parameters

goto_functions	GOTO functions to operate over. Must contain main.
ns	Namespace to operate in
target	Target to listen in on assigns/asserts/assumes. Is cloned.
context	Context to operate in.

◆ ~reachability_treet()

virtual reachability_treet::~reachability_treet ( )

virtualdefault

Default destructor.

Member Function Documentation

◆ check_for_hash_collision()

bool reachability_treet::check_for_hash_collision ( ) const

Check whether current ex_state is a state hash collision.

Returns: True if this state has already been visited

◆ check_thread_viable()

bool reachability_treet::check_thread_viable	(	unsigned int	tid,
		bool	quiet ) const

Determine if a thread can be run.

Checks that the thread has not already been explored from this frame, has not ended, has a non-empty call stack, and is not the monitor thread. Potentially prints a comment as to why the thread is blocked, for user feedback from get_ileave_direction_from_user

Parameters

tid	Thread ID to switch to
quiet	If false, will print to stdout why this thread is blocked

Returns: True if thread is viable; false otherwise.

◆ create_next_state()

void reachability_treet::create_next_state ( )

Perform context switch operation triggered elsewhere.

The analyse_* functions make a decision on whether or not to take a context switch, but defer the actual taking of this switch until later, to prevent switching with inconsistent state. This method causes that context switch, which has been decided upon, to actually be taken. As referred to in the reachability_treet algorithm, this makes up steps five and six.

◆ decide_ileave_direction()

unsigned int reachability_treet::decide_ileave_direction ( execution_statet & ex_state )

Pick a context switch to take.

Determines which thread to switch to now, according to whatever scheduling method/option is enabled. Called internally by various analysis routines.

Parameters

ex_state Execution state to analyse for switch direction

Returns: Thread ID of what thread to switch to next.

◆ dfs_explore_thread()

bool reachability_treet::dfs_explore_thread ( unsigned int tid )

protected

◆ drain_to_unexplored()

void reachability_treet::drain_to_unexplored ( bool add_leak_checks )

protected

Drain fully-explored frames from the top of exploration_frames until step_next_state finds an unexplored switch (or the stack empties).

If add_leak_checks is true, add memory-leak checks on the very last remaining frame before erasing it. On return, cur_frame_it points at the newly pushed top frame (the unexplored switch) when exploration_frames is non-empty.

◆ erase_current_frame()

void reachability_treet::erase_current_frame ( )

protected

◆ generate_schedule_formula()

goto_symext::symex_resultt reachability_treet::generate_schedule_formula ( )

Run threads in –schedule manner.

Run all threads to explore all interleavings, and encode it into a single trace.

Returns: Symex result representing all interleavings

◆ get_CS_bound()

int reachability_treet::get_CS_bound ( ) const

Permitted number of context switches to take.

Set with –context-bound <integer> on the command line. Paths where more than this many context switches occur will not be explored.

◆ get_cur_scheduler_frame() [1/2]

reachability_treet::scheduler_framet & reachability_treet::get_cur_scheduler_frame ( )

protected

◆ get_cur_scheduler_frame() [2/2]

const reachability_treet::scheduler_framet & reachability_treet::get_cur_scheduler_frame ( ) const

protected

◆ get_cur_state() [1/2]

execution_statet & reachability_treet::get_cur_state ( )

Return current execution_statet being explored / symex'd.

Returns: Current execution_statet being explored. Only valid while exploration_frames is non-empty. generate_schedule_formula() drains exploration_frames completely before returning, leaving cur_frame_it at exploration_frames.end() — do not call this (or get_cur_scheduler_frame()) after that point without first re-establishing a frame via setup_for_new_explore().

◆ get_cur_state() [2/2]

const execution_statet & reachability_treet::get_cur_state ( ) const

◆ get_ileave_direction_from_user()

int reachability_treet::get_ileave_direction_from_user ( ) const

Ask user for context switch to take.

Enabled with –interactive-ileaves. Prints out a list of current thread states, their stack traces and the current instruction being executed. Then ask the user what thread to switch to; giving feedback and asking again if that switch is blocked somehow.

Returns: Thread ID user desires us to switch to

◆ get_next_formula()

goto_symext::symex_resultt reachability_treet::get_next_formula ( )

Run threads to generate new trace.

Explores a new thread interleaving and returns its trace.

Returns: A symex_resultt recording the trace that we just generated.

◆ go_next_state()

void reachability_treet::go_next_state ( )

Advance to the next exploration frame, draining if we're at the top.

If there's already an exploration frame after the current one (we're in the middle of an existing interleaving), step onto it. Otherwise we're at the top of the stack: drain fully-explored frames via drain_to_unexplored, adding memory-leak checks on the very last frame before erasing it. Used by –schedule exploration.

◆ has_more_states()

bool reachability_treet::has_more_states ( )

Are there more execution_statet s to explore.

Returns: True if there are more execution_statet s to explore

◆ has_shared_lifetime()

bool reachability_treet::has_shared_lifetime ( const symbolt & s )

inlinestatic

Static or heap storage: shared however it is reached.

◆ is_address_taken_local()

bool reachability_treet::is_address_taken_local ( const irep_idt & name ) const

inline

◆ is_has_complete_formula()

bool reachability_treet::is_has_complete_formula ( )

Have we generated a full program trace.

Returns: True if all threads have run to completion

◆ is_shared_storage()

bool reachability_treet::is_shared_storage ( const symbolt & s ) const

inline

Static or heap storage, or a local whose address may reach a thread.

◆ mark_active_thread_explored()

void reachability_treet::mark_active_thread_explored ( )

Mark the active thread as already explored in the current scheduler frame.

◆ mark_search_truncated()

void reachability_treet::mark_search_truncated ( )

Record that the subtree below the frame being explored was cut short – by the context bound, by MPOR, by a state-hash collision, by an unwind bound truncating a loop, or by __ESBMC_switch_away_from – rather than exhausted.

Sleep sets are sound only over an exhausted subtree: skipping thread t at a node claims an already-explored schedule covers the interleaving, which a truncated search may never have produced. The two orders also differ in cost, so under –context-bound the covering schedule can need one context switch more than the budget allows.

Two cuts are knowingly excluded, both because marking them makes the reduction inert rather than merely weaker; see get_next_formula for why an unviable interleaving still loses no coverage, and note that the argument is about the active thread's guard, not the whole state's. check_if_ileaves_blocked's main-thread-ended rule is excluded because it fires on a property of the state rather than of the search order (#4584), so it cuts every branch alike: past that node no switch is honoured, each surviving thread runs as one transition, and a recorded footprint covers that thread's whole remaining access set – coarse enough that a conflicting thread wakes.

◆ may_be_written()

bool reachability_treet::may_be_written ( const irep_idt & name ) const

inline

True if name may be written by some thread somewhere in the program.

Conservatively returns true when the optimisation is disabled.

◆ post_hash_collision_cleanup()

void reachability_treet::post_hash_collision_cleanup ( )

Perform various pieces of accounting after a hash collision - primarily, ensuring that no further paths from this cswitch are explored.

◆ print_ileave_trace()

void reachability_treet::print_ileave_trace ( ) const

Prints state of execution_statet stack.

Primarily for debugging; takes the current stack of execution_statet s and prints a stack trace from the thread executing where the context switch was caused in each state. Gives you a good idea of how the current interleaving of ex_state shas been reached.

◆ remove_hash_collision_entry()

void reachability_treet::remove_hash_collision_entry ( )

Remove the current state's hash from the seen set.

Used when a transition is pruned by MPOR after its state hash has already been recorded, so that the seen set reflects the state explored before the pruned transition rather than the pruned state itself.

◆ report_reduction_stats()

void reachability_treet::report_reduction_stats ( ) const

Log the reduction counters.

Silent on a single-threaded run, which has no schedule space to report on.

◆ reset_to_unexplored_state()

bool reachability_treet::reset_to_unexplored_state ( )

Walks back to an unexplored context switch.

Follows the algorithm described in reachability_treet, and walk back up the stack of current exploration_frames to find a context-switch that hasn't yet been explored.

Returns: True if there are more states to be explored

◆ scan_address_taken()

void reachability_treet::scan_address_taken ( )

protected

Fill address_taken_globals and address_taken_locals from every body.

◆ scan_program_writes()

void reachability_treet::scan_program_writes ( )

protected

Walk all goto instructions once and collect the names of every global that may be written.

◆ setup_for_new_explore()

void reachability_treet::setup_for_new_explore ( )

Reinitialize for making new exploration of given functions.

Sets up the flags and fields of the object to start a new exploration of the goto functions we're operating over. To be called when the previous exploration using this object has been completed.

◆ setup_next_formula()

bool reachability_treet::setup_next_formula ( )

Reset ex_state stack to unexplored state.

This is just a wrapper around reset_to_unexplored_state

Returns: True if there is another state to be explored

◆ step_next_state()

bool reachability_treet::step_next_state ( )

Force a context switch, and take it.

Calls decide_ileave_direction, then create_next_state. The upshot of this is that if there is a context switch that could be taken, we find and take it. This implements steps 4-6 of the reachability_treet algorithm.

Returns: True if context switch was generated and taken

◆ switch_to_next_execution_state()

void reachability_treet::switch_to_next_execution_state ( )

Switch into just-generated execution state.

Run after a context switch has just been generated, switches current state to the newest one. Optionally generates more states if we were already on the last one (this may be un-needed).

◆ update_hash_collision_set()

void reachability_treet::update_hash_collision_set ( )

Update seen state hashes to contain current state.

◆ wake_dependent_sleepers()

void reachability_treet::wake_dependent_sleepers ( )

protected

Wake any sleeping thread the transition just taken is dependent on.

A no-op unless –sleep-sets is set.

◆ build_goto_symex_classes

void build_goto_symex_classes ( )

friend

◆ execution_statet

friend class execution_statet

friend

Member Data Documentation

◆ address_taken_globals

std::unordered_set<irep_idt, irep_id_hash> reachability_treet::address_taken_globals

protected

Globals whose address is taken anywhere in the program (including the global initialisers in __ESBMC_main).

ESBMC normalises every array/ function decay into an explicit address_of, so a global that never appears under an address_of can never enter any pointer's value set and therefore can never be the target of a write through a pointer.

◆ address_taken_locals

std::unordered_set<irep_idt, irep_id_hash> reachability_treet::address_taken_locals

protected

Non-static locals whose address is taken anywhere.

The pointer may reach another thread, so MPOR keys their accesses as it does a global's.

◆ any_indirect_write

bool reachability_treet::any_indirect_write = false

protected

Set when the static scan sees a write through a pointer it cannot resolve.

On its own this no longer disables the optimisation globally: an unresolved write can only land on a global whose address escaped, so may_be_written() gates this flag on address_taken_globals.

◆ CS_bound

int reachability_treet::CS_bound

protected

Limit on context switches; -1 for no limit.

◆ cs_bound_pruned

bool reachability_treet::cs_bound_pruned

–context-bound cut an available switch: the schedule space was truncated rather than exhausted (issue #6480).

◆ cur_frame_it

std::list<exploration_framet>::iterator reachability_treet::cur_frame_it

protected

Iterator recording the exploration frame we're operating on.

◆ directed_interleavings

bool reachability_treet::directed_interleavings

Functions dictate interleavings; perform no exploration.

Used by –directed-interleavings

◆ ever_written_globals

std::unordered_set<irep_idt, irep_id_hash> reachability_treet::ever_written_globals

protected

Static over-approximation of globals that may be written anywhere in the program.

Populated once at construction by scan_program_writes(). Used to skip context switches on variables that are only read across all threads.

◆ exploration_frames

std::list<exploration_framet> reachability_treet::exploration_frames

protected

Stack of exploration frames representing the current interleaving.

Each frame owns one execution state plus the scheduler bookkeeping for the context-switch point that led to it. The stack is initialized with a single frame containing the "main" state. During exploration it contains various numbers of frames; at the end it is empty.

See also: print_ileave_trace

◆ goto_functions

goto_functionst& reachability_treet::goto_functions

GOTO functions we're operating over.

◆ has_complete_formula

bool reachability_treet::has_complete_formula

Flag indicating we've executed all threads to exhaustion.

That is; for this particular interleaving. There may still be other interleavings to explore

◆ hit_hashes

std::unordered_map<std::size_t, int> reachability_treet::hit_hashes

protected

State hashes discovered, mapped to the smallest context-switch count at which each was seen.

A collision prunes only when the recorded cswitch is no greater than the current state's; pruning a state with more remaining budget would be unsound under –context-bound.

◆ interactive_ileaves

bool reachability_treet::interactive_ileaves

protected

Flag as to whether we're picking interleaving directions explicitly.

Corresponds to the –interactive-ileaves option.

◆ is_global

std::unordered_set<expr2tc, irep2_hash> reachability_treet::is_global

protected

◆ next_thread_id

unsigned int reachability_treet::next_thread_id

protected

Next thread ID to switch to, decided by analyse_* routines.

◆ ns

const namespacet& reachability_treet::ns

Namespace we're operating in.

◆ options

optionst& reachability_treet::options

Options that are enabled.

◆ permanent_context

contextt& reachability_treet::permanent_context

Context we're operating upon.

◆ por

bool reachability_treet::por

protected

Whether partial-order-reduction is enabled.

◆ readonly_global_opt

bool reachability_treet::readonly_global_opt = false

protected

Master switch; wired to –cswitch-skip-readonly-globals.

◆ reduction_stats

reduction_statst reachability_treet::reduction_stats

◆ schedule

bool reachability_treet::schedule

protected

Are we using the –schedule scheduling method?

◆ schedule_bounded_loop_truncations

unsigned int reachability_treet::schedule_bounded_loop_truncations

protected

Loops cut off at the unwinding bound in current –schedule exploration.

◆ schedule_remaining_claims

unsigned int reachability_treet::schedule_remaining_claims

protected

Number of remaining claims in current –schedule exploration.

◆ schedule_simplified_claims

unsigned int reachability_treet::schedule_simplified_claims

protected

Number of trivial claims in current –schedule exploration.

◆ schedule_target

std::shared_ptr<symex_targett> reachability_treet::schedule_target

protected

"Global" symex target for output from –schedule exploration

◆ schedule_total_claims

unsigned int reachability_treet::schedule_total_claims

protected

Number of claims in current –schedule exploration.

◆ sleep_sets

bool reachability_treet::sleep_sets

protected

Whether sleep sets prune the search (–sleep-sets).

◆ smt_during_symex

bool reachability_treet::smt_during_symex

protected

Are we using the –smt-during-symex method?

◆ state_hashing

bool reachability_treet::state_hashing

State hashing is enabled.

◆ target_template

std::shared_ptr<symex_targett> reachability_treet::target_template

protected

Target template; from which all targets are cloned.

This allows for the use of a non-concrete target class throughout exploration

◆ TS_slice

int reachability_treet::TS_slice

protected

Timeslice limit read from the "time-slice" option; currently unused.

◆ vars_map

std::unordered_map<expr2tc, std::list<unsigned int>, irep2_hash> reachability_treet::vars_map

protected

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

src/goto-symex/scheduler/reachability_tree.h
src/goto-symex/scheduler/reachability_tree.cpp
src/goto-symex/scheduler/reachability_tree_cin.cpp

Classes

Public Member Functions

Static Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Friends

Detailed Description

Constructor & Destructor Documentation

◆ reachability_treet()

◆ ~reachability_treet()

Member Function Documentation

◆ check_for_hash_collision()

◆ check_thread_viable()

◆ create_next_state()

◆ decide_ileave_direction()

◆ dfs_explore_thread()

◆ drain_to_unexplored()

◆ erase_current_frame()

◆ generate_schedule_formula()

◆ get_CS_bound()

◆ get_cur_scheduler_frame() [1/2]

◆ get_cur_scheduler_frame() [2/2]

◆ get_cur_state() [1/2]

◆ get_cur_state() [2/2]

◆ get_ileave_direction_from_user()

◆ get_next_formula()

◆ go_next_state()

◆ has_more_states()

◆ has_shared_lifetime()

◆ is_address_taken_local()

◆ is_has_complete_formula()

◆ is_shared_storage()

◆ mark_active_thread_explored()

◆ mark_search_truncated()

◆ may_be_written()

◆ post_hash_collision_cleanup()

◆ print_ileave_trace()

◆ remove_hash_collision_entry()

◆ report_reduction_stats()

◆ reset_to_unexplored_state()

◆ scan_address_taken()

◆ scan_program_writes()

◆ setup_for_new_explore()

◆ setup_next_formula()

◆ step_next_state()

◆ switch_to_next_execution_state()

◆ update_hash_collision_set()

◆ wake_dependent_sleepers()

Friends And Related Symbol Documentation

◆ build_goto_symex_classes

◆ execution_statet

Member Data Documentation

◆ address_taken_globals

◆ address_taken_locals

◆ any_indirect_write

◆ CS_bound

◆ cs_bound_pruned

◆ cur_frame_it

◆ directed_interleavings

◆ ever_written_globals

◆ exploration_frames

◆ goto_functions

◆ has_complete_formula

◆ hit_hashes

◆ interactive_ileaves

◆ is_global

◆ next_thread_id

◆ ns

◆ options

◆ permanent_context

◆ por

◆ readonly_global_opt

◆ reduction_stats

◆ schedule

◆ schedule_bounded_loop_truncations

◆ schedule_remaining_claims

◆ schedule_simplified_claims

◆ schedule_target

◆ schedule_total_claims