symabstract.hh File Reference

list segment based abstraction/concretization of heap objects More...

#include "config.h"
#include "symheap.hh"
#include <list>

Go to the source code of this file.

Typedefs
typedef std::list< SymHeap >	TSymHeapList
	container for symbolic heaps scheduled for processing.

Functions
void	concretizeObj (SymHeap &sh, TSymHeapList &dst, TObjId obj, ETargetSpecifier ts, TObjSet *leakObjs=0)
	concretize the given abstract object.
void	spliceOutListSegment (SymHeap &sh, TObjId seg, TObjSet *leakObjs)
	splice out a possibly empty list segment
void	dlSegReplaceByConcrete (SymHeap &sh, TObjId seg)
	replace a DLS by a single concrete object
void	abstractIfNeeded (SymHeap &sh)
	analyze the given symbolic heap and consider abstraction of some shapes that we know ho to rewrite to their more abstract way of existence
void	debugSymAbstract (bool enable)
	enable/disable debugging of symabstract

Detailed Description

list segment based abstraction/concretization of heap objects

Definition in file symabstract.hh.

Typedef Documentation

typedef std::list<SymHeap> TSymHeapList

container for symbolic heaps scheduled for processing.

It's feed by concretizeObj() and consumed by SymExecCore::concretizeLoop().

Definition at line 38 of file symabstract.hh.

Function Documentation

void abstractIfNeeded

(

SymHeap &

sh

)

analyze the given symbolic heap and consider abstraction of some shapes that we know ho to rewrite to their more abstract way of existence

Parameters

sh	an instance of symbolic heap, used in read/write mode

void concretizeObj	(	SymHeap &	sh,
		TSymHeapList &	dst,
		TObjId	obj,
		ETargetSpecifier	ts,
		TObjSet *	leakObjs = 0
	)

concretize the given abstract object.

If the result is non-deterministic, more than one symbolic heap can be produced.

Parameters

sh	an instance of symbolic heap, used in read/write mode
dst	a container for the results caused by non-deterministic decisions
obj	abstract heap object that should be concretized
ts	target specifier refining the target to be concretized
leakObjs	if not NULL, push all leaked root objects to the list

Note

the first result is always stored into sh, the use of dst is optional

void debugSymAbstract

(

bool

enable

)

enable/disable debugging of symabstract

void dlSegReplaceByConcrete	(	SymHeap &	sh,
		TObjId	seg
	)

replace a DLS by a single concrete object

void spliceOutListSegment	(	SymHeap &	sh,
		TObjId	seg,
		TObjSet *	leakObjs
	)

splice out a possibly empty list segment