reachability_treet::exploration_framet Struct Reference

#include <reachability_tree.h>

Public Attributes
std::shared_ptr< execution_statet >	state
scheduler_framet	scheduler
unsigned int	entered_via = UINT_MAX
	Thread whose switch created this frame; on backtracking it goes into the parent's sleep set.
bool	exhaustive = true
	Whether everything below this frame was actually explored.

Member Data Documentation

entered_via

unsigned int reachability_treet::exploration_framet::entered_via = UINT_MAX

Thread whose switch created this frame; on backtracking it goes into the parent's sleep set.

UINT_MAX for the root.

exhaustive

bool reachability_treet::exploration_framet::exhaustive = true

Whether everything below this frame was actually explored.

Cleared by any reduction that cut the subtree short, and propagated to the parent on backtracking. A sleep set may only record a thread whose subtree was exhausted – see mark_search_truncated.

scheduler

scheduler_framet reachability_treet::exploration_framet::scheduler

state

std::shared_ptr<execution_statet> reachability_treet::exploration_framet::state

---

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

• src/goto-symex/scheduler/reachability_tree.h