IndependentSolver.cpp File Reference

#include "klee/Solver/Solver.h"
#include "klee/Expr/Assignment.h"
#include "klee/Expr/Constraints.h"
#include "klee/Expr/Expr.h"
#include "klee/Expr/ExprUtil.h"
#include "klee/Support/Debug.h"
#include "klee/Solver/SolverImpl.h"
#include "llvm/Support/raw_ostream.h"
#include <list>
#include <map>
#include <ostream>
#include <vector>

Include dependency graph for IndependentSolver.cpp:

Go to the source code of this file.

Classes
class	DenseSet< T >
class	IndependentElementSet
class	IndependentSolver

Macros
#define	DEBUG_TYPE   "independent-solver"

Functions
template<class T >
llvm::raw_ostream &	operator<< (llvm::raw_ostream &os, const ::DenseSet< T > &dis)
llvm::raw_ostream &	operator<< (llvm::raw_ostream &os, const IndependentElementSet &ies)
static std::list< IndependentElementSet > *	getAllIndependentConstraintsSets (const Query &query)
static IndependentElementSet	getIndependentConstraints (const Query &query, std::vector< ref< Expr > > &result)
static void	calculateArrayReferences (const IndependentElementSet &ie, std::vector< const Array * > &returnVector)
bool	assertCreatedPointEvaluatesToTrue (const Query &query, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, std::map< const Array *, std::vector< unsigned char > > &retMap)

Macro Definition Documentation

DEBUG_TYPE

#define DEBUG_TYPE   "independent-solver"

Definition at line 10 of file IndependentSolver.cpp.

Function Documentation

assertCreatedPointEvaluatesToTrue()

bool assertCreatedPointEvaluatesToTrue	(	const Query &	query,
		const std::vector< const Array * > &	objects,
		std::vector< std::vector< unsigned char > > &	values,
		std::map< const Array *, std::vector< unsigned char > > &	retMap
	)

Definition at line 440 of file IndependentSolver.cpp.

References klee::Assignment::bindings, klee::Query::constraints, klee::Assignment::evaluate(), and klee::Query::expr.

Referenced by IndependentSolver::computeInitialValues().

Here is the call graph for this function:

Here is the caller graph for this function:

calculateArrayReferences()

static void calculateArrayReferences ( const IndependentElementSet &  ie, std::vector< const Array * > &  returnVector  )

static

Definition at line 372 of file IndependentSolver.cpp.

References IndependentElementSet::elements, and IndependentElementSet::wholeObjects.

Referenced by IndependentSolver::computeInitialValues().

Here is the caller graph for this function:

getAllIndependentConstraintsSets()

static std::list< IndependentElementSet > * getAllIndependentConstraintsSets ( const Query &  query )

static

Definition at line 263 of file IndependentSolver.cpp.

References IndependentElementSet::add(), klee::Query::constraints, klee::Query::expr, IndependentElementSet::intersects(), and klee::ConstantExpr::isFalse().

Referenced by IndependentSolver::computeInitialValues().

Here is the call graph for this function:

Here is the caller graph for this function:

getIndependentConstraints()

static IndependentElementSet getIndependentConstraints ( const Query &  query, std::vector< ref< Expr > > &  result  )

static

Definition at line 321 of file IndependentSolver.cpp.

References IndependentElementSet::add(), klee::Query::constraints, and klee::Query::expr.

Referenced by IndependentSolver::computeTruth(), IndependentSolver::computeValidity(), and IndependentSolver::computeValue().

Here is the call graph for this function:

Here is the caller graph for this function:

operator<<() [1/2]

template<class T >

llvm::raw_ostream & operator<< ( llvm::raw_ostream &  os, const ::DenseSet< T > &  dis  )

inline

Definition at line 92 of file IndependentSolver.cpp.

operator<<() [2/2]

llvm::raw_ostream & operator<< ( llvm::raw_ostream &  os, const IndependentElementSet &  ies  )

inline

Definition at line 252 of file IndependentSolver.cpp.

References IndependentElementSet::print().

Here is the call graph for this function: