Description

Feasible path analysis.

Determines whether CFG paths are feasible paths.

Definition at line 23 of file FeasiblePath.h.

#include <Rose/BinaryAnalysis/FeasiblePath.h>

Collaboration diagram for Rose::BinaryAnalysis::FeasiblePath:

[legend]

Classes
class	Exception
	Exception for errors specific to feasible path analysis. More...

struct	Expression
	Expression to be evaluated. More...

class	FunctionSummarizer
	Base class for callbacks for function summaries. More...

struct	FunctionSummary
	Information stored per V_USER_DEFINED path vertex. More...

class	PathProcessor
	Path searching functor. More...

struct	Settings
	Settings that control this analysis. More...

struct	Statistics
	Statistics from path searching. More...

struct	VarDetail
	Information about a variable seen on a path. More...

Public Types
enum	SearchMode { SEARCH_SINGLE_DFS , SEARCH_SINGLE_BFS , SEARCH_MULTI }
	How to search for paths. More...

enum	SemanticMemoryParadigm { LIST_BASED_MEMORY , MAP_BASED_MEMORY }
	Organization of semantic memory. More...

enum	EdgeVisitOrder { VISIT_NATURAL , VISIT_REVERSE , VISIT_RANDOM }
	Edge visitation order. More...

enum	IoMode { READ , WRITE }
	Read or write operation. More...

enum	MayOrMust { MAY , MUST }
	Types of comparisons. More...

typedef std::set< rose_addr_t >	AddressSet
	Set of basic block addresses.

typedef Sawyer::Container::Map< std::string, FeasiblePath::VarDetail >	VarDetails
	Variable detail by name.

typedef Sawyer::Container::Map< rose_addr_t, FunctionSummary >	FunctionSummaries
	Summaries for multiple functions.

Public Member Functions
	FeasiblePath ()
	Constructs a new feasible path analyzer.

void	reset ()
	Reset to initial state without changing settings.

void	resetStatistics ()
	Reset only statistics.

virtual InstructionSemantics::BaseSemantics::DispatcherPtr	buildVirtualCpu (const Partitioner2::PartitionerConstPtr &, const Partitioner2::CfgPath , PathProcessor , const SmtSolverPtr &)
	Create the virtual CPU.

virtual void	setInitialState (const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu, const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsBeginVertex)
	Initialize state for first vertex of path.

virtual void	processBasicBlock (const Partitioner2::BasicBlockPtr &bblock, const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu, size_t pathInsnIndex)
	Process instructions for one basic block on the specified virtual CPU.

virtual void	processIndeterminateBlock (const Partitioner2::ControlFlowGraph::ConstVertexIterator &vertex, const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu, size_t pathInsnIndex)
	Process an indeterminate block.

virtual void	processFunctionSummary (const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsVertex, const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu, size_t pathInsnIndex)
	Process a function summary vertex.

virtual void	processVertex (const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu, const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsVertex, size_t pathInsnIndex)
	Process one vertex.

virtual bool	shouldSummarizeCall (const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathVertex, const Partitioner2::ControlFlowGraph &cfg, const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgCallTarget)
	Determines whether a function call should be summarized instead of inlined.

virtual bool	shouldInline (const Partitioner2::CfgPath &path, const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgCallTarget)
	Determines whether a function call should be inlined.

Partitioner2::ControlFlowGraph::ConstVertexIterator	pathToCfg (const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathVertex) const
	Convert path vertex to a CFG vertex.

Partitioner2::CfgConstVertexSet	cfgToPaths (const Partitioner2::CfgConstVertexSet &) const
	Convert CFG vertices to path vertices.

Partitioner2::CfgConstEdgeSet	cfgToPaths (const Partitioner2::CfgConstEdgeSet &) const
	Convert CFG edges to path edges.

bool	pathEndsWithFunctionCall (const Partitioner2::CfgPath &) const
	True if path ends with a function call.

bool	isFunctionCall (const Partitioner2::ControlFlowGraph::ConstVertexIterator &) const
	True if vertex is a function call.

void	printPathVertex (std::ostream &out, const Partitioner2::ControlFlowGraph::Vertex &pathVertex, size_t &insnIdx) const
	Print one vertex of a path for debugging.

void	printPath (std::ostream &out, const Partitioner2::CfgPath &) const
	Print the path to the specified output stream.

bool	isAnyEndpointReachable (const Partitioner2::ControlFlowGraph &cfg, const Partitioner2::ControlFlowGraph::ConstVertexIterator &beginVertex, const Partitioner2::CfgConstVertexSet &endVertices)
	Determine whether any ending vertex is reachable.

bool	isDirectedSearch () const
	Property: Whether search is directed or not.

void	depthFirstSearch (PathProcessor &pathProcessor)
	Find all feasible paths.

Partitioner2::PartitionerConstPtr	partitioner () const
	Property: Partitioner currently in use.

const FunctionSummaries &	functionSummaries () const
	Function summary information.

const FunctionSummary &	functionSummary (rose_addr_t entryVa) const
	Function summary information.

const VarDetail &	varDetail (const InstructionSemantics::BaseSemantics::StatePtr &, const std::string &varName) const
	Details about a variable.

const VarDetails &	varDetails (const InstructionSemantics::BaseSemantics::StatePtr &) const
	Details about all variables by name.

InstructionSemantics::BaseSemantics::StatePtr	initialState () const
	Get the initial state before the first path vertex.

double	pathEffectiveK (const Partitioner2::CfgPath &) const
	Effective maximum path length.

Statistics	statistics () const
	Cumulative statistics about prior analyses.


const Settings &	settings () const
	Property: Settings used by this analysis.

Settings &	settings ()
	Property: Settings used by this analysis.

void	settings (const Settings &s)
	Property: Settings used by this analysis.


FunctionSummarizer::Ptr	functionSummarizer () const
	Property: Function summary handling.

void	functionSummarizer (const FunctionSummarizer::Ptr &f)
	Property: Function summary handling.


void	setSearchBoundary (const Partitioner2::PartitionerConstPtr &partitioner, const Partitioner2::CfgConstVertexSet &cfgBeginVertices, const Partitioner2::CfgConstVertexSet &cfgEndVertices, const Partitioner2::CfgConstVertexSet &cfgAvoidVertices=Partitioner2::CfgConstVertexSet(), const Partitioner2::CfgConstEdgeSet &cfgAvoidEdges=Partitioner2::CfgConstEdgeSet())
	Specify search boundary.

void	setSearchBoundary (const Partitioner2::PartitionerConstPtr &partitioner, const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgBeginVertex, const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgEndVertex, const Partitioner2::CfgConstVertexSet &cfgAvoidVertices=Partitioner2::CfgConstVertexSet(), const Partitioner2::CfgConstEdgeSet &cfgAvoidEdges=Partitioner2::CfgConstEdgeSet())
	Specify search boundary.

void	setSearchBoundary (const Partitioner2::PartitionerConstPtr &partitioner, const Partitioner2::CfgConstVertexSet &cfgBeginVertices, const Partitioner2::CfgConstVertexSet &cfgAvoidVertices=Partitioner2::CfgConstVertexSet(), const Partitioner2::CfgConstEdgeSet &cfgAvoidEdges=Partitioner2::CfgConstEdgeSet())
	Specify search boundary.

void	setSearchBoundary (const Partitioner2::PartitionerConstPtr &partitioner, const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgBeginVertex, const Partitioner2::CfgConstVertexSet &cfgAvoidVertices=Partitioner2::CfgConstVertexSet(), const Partitioner2::CfgConstEdgeSet &cfgAvoidEdges=Partitioner2::CfgConstEdgeSet())
	Specify search boundary.

Static Public Member Functions
static void	initDiagnostics ()
	Initialize diagnostic output.

static Sawyer::CommandLine::SwitchGroup	commandLineSwitches (Settings &settings)
	Describe command-line switches.

static std::string	expressionDocumentation ()
	Documentation for the symbolic expression parser.

static InstructionSemantics::BaseSemantics::StatePtr	pathPostState (const Partitioner2::CfgPath &, size_t vertexIdx)
	Get the state at the end of the specified vertex.

static size_t	pathLength (const Partitioner2::CfgPath &, int position=-1)
	Total length of path up to and including the specified vertex.

Public Attributes
RegisterDescriptor	REG_PATH
	Descriptor of path pseudo-registers.

Static Public Attributes
static Sawyer::Message::Facility	mlog
	Diagnostic output.

Member Typedef Documentation

◆ AddressSet

typedef std::set<rose_addr_t> Rose::BinaryAnalysis::FeasiblePath::AddressSet

Set of basic block addresses.

Definition at line 63 of file FeasiblePath.h.

◆ VarDetails

typedef Sawyer::Container::Map<std::string , FeasiblePath::VarDetail> Rose::BinaryAnalysis::FeasiblePath::VarDetails

Variable detail by name.

Definition at line 173 of file FeasiblePath.h.

◆ FunctionSummaries

typedef Sawyer::Container::Map<rose_addr_t, FunctionSummary> Rose::BinaryAnalysis::FeasiblePath::FunctionSummaries

Summaries for multiple functions.

Definition at line 305 of file FeasiblePath.h.

Member Enumeration Documentation

◆ SearchMode

enum Rose::BinaryAnalysis::FeasiblePath::SearchMode

How to search for paths.

Enumerator
SEARCH_SINGLE_DFS	Perform a depth first search.
SEARCH_SINGLE_BFS	Perform a breadth first search.
SEARCH_MULTI	Blast everything at once to the SMT solver.

Definition at line 37 of file FeasiblePath.h.

◆ SemanticMemoryParadigm

enum Rose::BinaryAnalysis::FeasiblePath::SemanticMemoryParadigm

Organization of semantic memory.

Enumerator
LIST_BASED_MEMORY	Precise but slow.
MAP_BASED_MEMORY	Fast but not precise.

Definition at line 44 of file FeasiblePath.h.

◆ EdgeVisitOrder

enum Rose::BinaryAnalysis::FeasiblePath::EdgeVisitOrder

Edge visitation order.

Enumerator
VISIT_NATURAL	Visit edges in their natural, forward order.
VISIT_REVERSE	Visit edges in reverse of the natural order.
VISIT_RANDOM	Visit edges in random order.

Definition at line 50 of file FeasiblePath.h.

◆ IoMode

enum Rose::BinaryAnalysis::FeasiblePath::IoMode

Read or write operation.

Definition at line 57 of file FeasiblePath.h.

◆ MayOrMust

enum Rose::BinaryAnalysis::FeasiblePath::MayOrMust

Types of comparisons.

Definition at line 60 of file FeasiblePath.h.

Member Function Documentation

◆ resetStatistics()

void Rose::BinaryAnalysis::FeasiblePath::resetStatistics ( )

inline

Reset only statistics.

Thread safety: This method is thread safe.

Definition at line 377 of file FeasiblePath.h.

◆ initDiagnostics()

static void Rose::BinaryAnalysis::FeasiblePath::initDiagnostics ( )

static

Initialize diagnostic output.

This is called automatically when ROSE is initialized.

◆ settings() [1/3]

const Settings & Rose::BinaryAnalysis::FeasiblePath::settings ( ) const

inline

Property: Settings used by this analysis.

Definition at line 393 of file FeasiblePath.h.

◆ settings() [2/3]

Settings & Rose::BinaryAnalysis::FeasiblePath::settings ( )

inline

Property: Settings used by this analysis.

Definition at line 394 of file FeasiblePath.h.

◆ settings() [3/3]

void Rose::BinaryAnalysis::FeasiblePath::settings ( const Settings & s )

inline

Property: Settings used by this analysis.

Definition at line 395 of file FeasiblePath.h.

◆ commandLineSwitches()

static Sawyer::CommandLine::SwitchGroup Rose::BinaryAnalysis::FeasiblePath::commandLineSwitches ( Settings & settings )

static

Describe command-line switches.

The settings provide default values. A reference to settings is saved and when the command-line is parsed and applied, the settings are adjusted.

◆ buildVirtualCpu()

virtual InstructionSemantics::BaseSemantics::DispatcherPtr Rose::BinaryAnalysis::FeasiblePath::buildVirtualCpu	(	const Partitioner2::PartitionerConstPtr &	,
		const Partitioner2::CfgPath *	,
		PathProcessor *	,
		const SmtSolverPtr &
	)

virtual

Create the virtual CPU.

Creates a new virtual CPU for each call. The first call also makes a copy of the register dictionary from the specified partitioner and augments it with a "path" pseudo-register that holds a symbolic expressions on which the current CFG path depends.

◆ setInitialState()

virtual void Rose::BinaryAnalysis::FeasiblePath::setInitialState	(	const InstructionSemantics::BaseSemantics::DispatcherPtr &	cpu,
		const Partitioner2::ControlFlowGraph::ConstVertexIterator &	pathsBeginVertex
	)

virtual

Initialize state for first vertex of path.

Given the beginning of the path and the virtual CPU, initialize that state with whatever is suitable for the analysis. The default implementation sets the "path" pseudo-register to true (since the first vertex of the path is unconditionally feasible), sets the instruction pointer register to the first instruction, and initializes the stack pointer with the concrete stack pointer from settings (if any). On x86, the DF register is set.

◆ processBasicBlock()

virtual void Rose::BinaryAnalysis::FeasiblePath::processBasicBlock	(	const Partitioner2::BasicBlockPtr &	bblock,
		const InstructionSemantics::BaseSemantics::DispatcherPtr &	cpu,
		size_t	pathInsnIndex
	)

virtual

Process instructions for one basic block on the specified virtual CPU.

This is a state transfer function, updating the virtual machine state by processing the instructions of the specified basic block.

◆ processIndeterminateBlock()

virtual void Rose::BinaryAnalysis::FeasiblePath::processIndeterminateBlock	(	const Partitioner2::ControlFlowGraph::ConstVertexIterator &	vertex,
		const InstructionSemantics::BaseSemantics::DispatcherPtr &	cpu,
		size_t	pathInsnIndex
	)

virtual

Process an indeterminate block.

This is a state transfer function, representing flow of control through an unknown address.

◆ processFunctionSummary()

virtual void Rose::BinaryAnalysis::FeasiblePath::processFunctionSummary	(	const Partitioner2::ControlFlowGraph::ConstVertexIterator &	pathsVertex,
		const InstructionSemantics::BaseSemantics::DispatcherPtr &	cpu,
		size_t	pathInsnIndex
	)

virtual

Process a function summary vertex.

This is a state transfer function, representing flow of control across a summarized function.

◆ processVertex()

virtual void Rose::BinaryAnalysis::FeasiblePath::processVertex	(	const InstructionSemantics::BaseSemantics::DispatcherPtr &	cpu,
		const Partitioner2::ControlFlowGraph::ConstVertexIterator &	pathsVertex,
		size_t	pathInsnIndex
	)

virtual

Process one vertex.

This is the general state transfer function, representing flow of control through any type of vertex.

◆ functionSummarizer() [1/2]

FunctionSummarizer::Ptr Rose::BinaryAnalysis::FeasiblePath::functionSummarizer ( ) const

inline

Property: Function summary handling.

As an alternative to creating a subclass to override the processFunctionSummary, this property can contain an object that will be called in various ways whenever a function summary is processed. If non-null, then whenever a function summary is created, the object's init method is called, and whenever a function summary is traversed its process method is called.

Definition at line 480 of file FeasiblePath.h.

◆ functionSummarizer() [2/2]

void Rose::BinaryAnalysis::FeasiblePath::functionSummarizer ( const FunctionSummarizer::Ptr & f )

inline

Property: Function summary handling.

As an alternative to creating a subclass to override the processFunctionSummary, this property can contain an object that will be called in various ways whenever a function summary is processed. If non-null, then whenever a function summary is created, the object's init method is called, and whenever a function summary is traversed its process method is called.

Definition at line 481 of file FeasiblePath.h.

◆ cfgToPaths()

Partitioner2::CfgConstEdgeSet Rose::BinaryAnalysis::FeasiblePath::cfgToPaths ( const Partitioner2::CfgConstEdgeSet & ) const

Convert CFG edges to path edges.

Any edges that don't exist in the paths graph are ignored and not returned.

◆ printPath()

void Rose::BinaryAnalysis::FeasiblePath::printPath	(	std::ostream &	out,
		const Partitioner2::CfgPath &
	)		const

Print the path to the specified output stream.

This is intended mainly for debugging.

◆ isAnyEndpointReachable()

bool Rose::BinaryAnalysis::FeasiblePath::isAnyEndpointReachable	(	const Partitioner2::ControlFlowGraph &	cfg,
		const Partitioner2::ControlFlowGraph::ConstVertexIterator &	beginVertex,
		const Partitioner2::CfgConstVertexSet &	endVertices
	)

Determine whether any ending vertex is reachable.

Returns true if any of the endVertices can be reached from the beginVertex by following the edges of the graph. However, if isDirectedSearch is false, then the end vertices are ignored and this function always returns true.

◆ setSearchBoundary() [1/4]

void Rose::BinaryAnalysis::FeasiblePath::setSearchBoundary	(	const Partitioner2::PartitionerConstPtr &	partitioner,
		const Partitioner2::CfgConstVertexSet &	cfgBeginVertices,
		const Partitioner2::CfgConstVertexSet &	cfgEndVertices,
		const Partitioner2::CfgConstVertexSet &	cfgAvoidVertices = `Partitioner2::CfgConstVertexSet()`,
		const Partitioner2::CfgConstEdgeSet &	cfgAvoidEdges = `Partitioner2::CfgConstEdgeSet()`
	)

Specify search boundary.

This function initializes the analysis by specifying starting and ending CFG vertices and the vertices and edges that should be avoided. If the cfgEndVertices is supplied (even if empty) then the search is directed. A directed search considers only the subset of the CFG that consists of vertices and edges that appear on some path from any of the cfgBeginVertices to any of the cfgEndVertices.

◆ setSearchBoundary() [2/4]

void Rose::BinaryAnalysis::FeasiblePath::setSearchBoundary	(	const Partitioner2::PartitionerConstPtr &	partitioner,
		const Partitioner2::ControlFlowGraph::ConstVertexIterator &	cfgBeginVertex,
		const Partitioner2::ControlFlowGraph::ConstVertexIterator &	cfgEndVertex,
		const Partitioner2::CfgConstVertexSet &	cfgAvoidVertices = `Partitioner2::CfgConstVertexSet()`,
		const Partitioner2::CfgConstEdgeSet &	cfgAvoidEdges = `Partitioner2::CfgConstEdgeSet()`
	)

Specify search boundary.

This function initializes the analysis by specifying starting and ending CFG vertices and the vertices and edges that should be avoided. If the cfgEndVertices is supplied (even if empty) then the search is directed. A directed search considers only the subset of the CFG that consists of vertices and edges that appear on some path from any of the cfgBeginVertices to any of the cfgEndVertices.

◆ setSearchBoundary() [3/4]

void Rose::BinaryAnalysis::FeasiblePath::setSearchBoundary	(	const Partitioner2::PartitionerConstPtr &	partitioner,
		const Partitioner2::CfgConstVertexSet &	cfgBeginVertices,
		const Partitioner2::CfgConstVertexSet &	cfgAvoidVertices = `Partitioner2::CfgConstVertexSet()`,
		const Partitioner2::CfgConstEdgeSet &	cfgAvoidEdges = `Partitioner2::CfgConstEdgeSet()`
	)

Specify search boundary.

This function initializes the analysis by specifying starting and ending CFG vertices and the vertices and edges that should be avoided. If the cfgEndVertices is supplied (even if empty) then the search is directed. A directed search considers only the subset of the CFG that consists of vertices and edges that appear on some path from any of the cfgBeginVertices to any of the cfgEndVertices.

◆ setSearchBoundary() [4/4]

void Rose::BinaryAnalysis::FeasiblePath::setSearchBoundary	(	const Partitioner2::PartitionerConstPtr &	partitioner,
		const Partitioner2::ControlFlowGraph::ConstVertexIterator &	cfgBeginVertex,
		const Partitioner2::CfgConstVertexSet &	cfgAvoidVertices = `Partitioner2::CfgConstVertexSet()`,
		const Partitioner2::CfgConstEdgeSet &	cfgAvoidEdges = `Partitioner2::CfgConstEdgeSet()`
	)

Specify search boundary.

This function initializes the analysis by specifying starting and ending CFG vertices and the vertices and edges that should be avoided. If the cfgEndVertices is supplied (even if empty) then the search is directed. A directed search considers only the subset of the CFG that consists of vertices and edges that appear on some path from any of the cfgBeginVertices to any of the cfgEndVertices.

◆ isDirectedSearch()

bool Rose::BinaryAnalysis::FeasiblePath::isDirectedSearch ( ) const

inline

Property: Whether search is directed or not.

A directed search attempts to find a path that reaches one of a set of goal vertices, set by the setSearchBoundary functions that take a cfgEndVertex or cfgEndVertices argument. On the other hand, an undirected search just keeps following paths to explore the entire execution space.

Definition at line 567 of file FeasiblePath.h.

◆ depthFirstSearch()

void Rose::BinaryAnalysis::FeasiblePath::depthFirstSearch ( PathProcessor & pathProcessor )

Find all feasible paths.

Searches for paths and calls the pathProcessor each time a feasible path is found. The space is explored using a depth first search, and the search can be limited with various settings.

◆ partitioner()

Partitioner2::PartitionerConstPtr Rose::BinaryAnalysis::FeasiblePath::partitioner ( ) const

Property: Partitioner currently in use.

Returns a reference to the partitioner that is currently in use, set by setSearchBoundary. It is a fatal error to call this function if there is no partitioner.

◆ functionSummaries()

const FunctionSummaries & Rose::BinaryAnalysis::FeasiblePath::functionSummaries ( ) const

inline

Function summary information.

This is a map of functions that have been summarized, indexed by function entry address.

Definition at line 595 of file FeasiblePath.h.

◆ functionSummary()

const FunctionSummary & Rose::BinaryAnalysis::FeasiblePath::functionSummary ( rose_addr_t entryVa ) const

Function summary information.

This is the summary information for a single function. If the specified function is not summarized then a default-constructed summary information object is returned.

◆ pathEffectiveK()

double Rose::BinaryAnalysis::FeasiblePath::pathEffectiveK ( const Partitioner2::CfgPath & ) const

Effective maximum path length.

Returns the effective maximum path length, k, for the specified path. The maximum is based on the maxPathLength property, but adjusted up or down as vertices are added to the path. The adjusted values are stored as attributes of the path, and this function returns the current value.

◆ pathLength()

static size_t Rose::BinaryAnalysis::FeasiblePath::pathLength	(	const Partitioner2::CfgPath &	,
		int	position = `-1`
	)

static

Total length of path up to and including the specified vertex.

The path length is different than the number of vertices (Partitioner2::CfgPath::nVertices). Path length is measured by summing the sizes of all the vertices. The size of a vertex that represents a basic block is the number of instructions in that basic block. The path length is what's used to limit the depth of the search in k-bounded model checking.

◆ statistics()

Statistics Rose::BinaryAnalysis::FeasiblePath::statistics ( ) const

inline

Cumulative statistics about prior analyses.

These statistics accumulate across all analysis calls and can be reset by either reset or resetStatistics.

Thread safety: This method is thread safe.

Definition at line 637 of file FeasiblePath.h.

Member Data Documentation

◆ mlog

Sawyer::Message::Facility Rose::BinaryAnalysis::FeasiblePath::mlog

static

Diagnostic output.

Definition at line 146 of file FeasiblePath.h.

◆ REG_PATH

RegisterDescriptor Rose::BinaryAnalysis::FeasiblePath::REG_PATH

Descriptor of path pseudo-registers.

This analysis adds a special register named "path" to the register dictionary. This register holds the expression that determines how to reach the end of the path from the beginning. The major and minor numbers are arbitrary, but chosen so that they hopefully don't conflict with any real registers, which tend to start counting at zero. Since we're using BaseSemantics::RegisterStateGeneric, we can use its flexibility to store extra "registers" without making any other changes to the architecture.

Definition at line 155 of file FeasiblePath.h.

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

FeasiblePath.h

Description

Classes

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Static Public Attributes

Member Typedef Documentation

◆ AddressSet

◆ VarDetails

◆ FunctionSummaries

Member Enumeration Documentation

◆ SearchMode

◆ SemanticMemoryParadigm

◆ EdgeVisitOrder

◆ IoMode

◆ MayOrMust

Member Function Documentation

◆ resetStatistics()

◆ initDiagnostics()

◆ settings() [1/3]

◆ settings() [2/3]

◆ settings() [3/3]

◆ commandLineSwitches()

◆ buildVirtualCpu()

◆ setInitialState()

◆ processBasicBlock()

◆ processIndeterminateBlock()

◆ processFunctionSummary()

◆ processVertex()

◆ functionSummarizer() [1/2]

◆ functionSummarizer() [2/2]

◆ cfgToPaths()

◆ printPath()

◆ isAnyEndpointReachable()

◆ setSearchBoundary() [1/4]

◆ setSearchBoundary() [2/4]

◆ setSearchBoundary() [3/4]

◆ setSearchBoundary() [4/4]

◆ isDirectedSearch()

◆ depthFirstSearch()

◆ partitioner()

◆ functionSummaries()

◆ functionSummary()

◆ pathEffectiveK()

◆ pathLength()

◆ statistics()

Member Data Documentation

◆ mlog

◆ REG_PATH