A search stack entry, used in tracking nodes to mark reachable when walking over the CFG in fixedpoint_to_assertions and fixedpoint_from_assertions. More...

#include <reachability_slicer_class.h>

Public Member Functions
	search_stack_entryt (cfgt::node_indext node_index, bool caller_is_known)

Public Attributes
cfgt::node_indext	node_index
	CFG node to mark reachable. More...

bool	caller_is_known
	If true, this function's caller is known and has already been queued to mark reachable, so there is no need to queue anything when walking out of the function, whether forwards (via END_FUNCTION) or backwards (via a callsite). More...

Detailed Description

A search stack entry, used in tracking nodes to mark reachable when walking over the CFG in fixedpoint_to_assertions and fixedpoint_from_assertions.

Definition at line 54 of file reachability_slicer_class.h.

Constructor & Destructor Documentation

◆ search_stack_entryt()

reachability_slicert::search_stack_entryt::search_stack_entryt	(	cfgt::node_indext	node_index,
		bool	caller_is_known
	)

inline

Definition at line 68 of file reachability_slicer_class.h.

Member Data Documentation

◆ caller_is_known

bool reachability_slicert::search_stack_entryt::caller_is_known

If true, this function's caller is known and has already been queued to mark reachable, so there is no need to queue anything when walking out of the function, whether forwards (via END_FUNCTION) or backwards (via a callsite).

If false, this function's caller is not known, so when walking forwards from the end or backwards from the beginning we should queue all possible callers.

Definition at line 66 of file reachability_slicer_class.h.

◆ node_index

cfgt::node_indext reachability_slicert::search_stack_entryt::node_index

CFG node to mark reachable.

Definition at line 57 of file reachability_slicer_class.h.

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

/home/runner/work/cbmc/cbmc/src/goto-instrument/reachability_slicer_class.h