symtrace.hh File Reference

directed acyclic graph of the symbolic execution trace, see namespace Trace More...

#include "config.h"
#include "id_mapper.hh"
#include "join_status.hh"
#include "symbt.hh"
#include "symheap.hh"
#include <vector>
#include <string>

Go to the source code of this file.

Data Structures
class	NodeBase
	an abstract base for Node and NodeHandle (externally not much useful) More...
class	Node
	an abstract node of the symbolic execution trace graph More...
class	NodeHandle
	useful to prevent a trace sub-graph from being destroyed too early More...
class	TransientNode
	used to explicitly highlight trace graph nodes that should not be reachable More...
class	RootNode
	root node of the trace graph (usually a call of the root function) More...
class	InsnNode
	a trace graph node that represents a non-terminal instruction More...
class	CondNode
	a trace graph node that represents a conditional insn being traversed More...
class	AbstractionNode
	a trace graph node that represents a single abstraction step More...
class	ConcretizationNode
	a trace graph node that represents a single concretization step More...
class	SpliceOutNode
	a trace graph node that represents a single splice-out operation More...
class	JoinNode
	a trace graph node that represents a single join operation More...
class	CloneNode
	trace graph nodes inserted automatically per each SymHeap clone operation More...
class	CallEntryNode
	trace graph node representing a call entry point More...
class	CallCacheHitNode
	trace graph node representing a cached call result More...
class	CallFrameNode
	trace graph node representing a call frame More...
class	CallDoneNode
	trace graph node representing a call result More...
class	ImportGlVarNode
	a trace graph node that represents a single call of importGlVar() More...
class	MsgNode
	trace graph node representing an error/warning message More...
class	UserNode
	trace graph node representing something important for the user More...
class	EndPointConsolidator
	a container maintaining a set of trace graph end-points More...
class	GraphProxy
	a container maintaining a set of trace graphs being built on the fly More...
class	Globals
	a singleton holding global GraphProxy (may be extended later) More...

Namespaces
namespace	CodeStorage
	object model that describes the analyzed code on the input
namespace	Trace
	directed acyclic graph of the symbolic execution trace

Typedefs
typedef struct cl_loc *	TLoc
typedef const CodeStorage::Fnc *	TFnc
typedef const CodeStorage::Insn *	TInsn
typedef std::vector< Node * >	TNodeList
typedef IdMapper< TObjId, OBJ_INVALID, OBJ_MAX_ID >	TIdMapper
typedef std::vector< TIdMapper >	TIdMapperList

Functions
std::string	insnToLabel (const TInsn insn)
void	replaceNode (Node *tr, Node *by)
void	resolveIdMapping (TIdMapper *pDst, const Node *trSrc, const Node *trDst)
	resolve composite ID mapping from trSrc to trDst
bool	plotTrace (Node *endPoint, const std::string &name, std::string *pName=0)
	plot a trace graph named "name-NNNN.dot" leading to the given node
void	printTrace (Node *endPoint)
	print a human-readable trace using the Code Listener messaging API
bool	chkTraceGraphConsistency (Node *const from)
	this runs in the debug build only
void	waiveCloneOperation (SymHeap &sh)
	mark the just completed clone operation as intended and unimportant
void	waiveCloneOperation (SymState &)
	mark the just completed clone operation as intended and unimportant

Detailed Description

directed acyclic graph of the symbolic execution trace, see namespace Trace

Definition in file symtrace.hh.