klee::ImpliedValue Namespace Reference

Functions
void	getImpliedValues (ref< Expr > e, ref< ConstantExpr > cvalue, ImpliedValueList &result)
void	checkForImpliedValues (Solver *S, ref< Expr > e, ref< ConstantExpr > cvalue)

Function Documentation

checkForImpliedValues()

void klee::ImpliedValue::checkForImpliedValues	(	Solver *	S,
		ref< Expr >	e,
		ref< ConstantExpr >	cvalue
	)

Definition at line 188 of file ImpliedValue.cpp.

References klee::findReads(), getImpliedValues(), klee::Solver::getValue(), klee::ReadExpr::index, klee::Solver::mustBeTrue(), klee::ConstraintSet::push_back(), klee::UpdateList::root, klee::Array::size, and klee::ReadExpr::updates.

Referenced by klee::Executor::doImpliedValueConcretization().

Here is the call graph for this function:

Here is the caller graph for this function:

getImpliedValues()

void klee::ImpliedValue::getImpliedValues	(	ref< Expr >	e,
		ref< ConstantExpr >	cvalue,
		ImpliedValueList &	result
	)

Definition at line 27 of file ImpliedValue.cpp.

References klee::SelectExpr::cond, klee::SelectExpr::falseExpr, getImpliedValues(), klee::ConcatExpr::getKid(), klee::Expr::getKind(), klee::Expr::getWidth(), klee::BinaryExpr::left, klee::BinaryExpr::right, klee::CastExpr::src, klee::Expr::Sub, and klee::SelectExpr::trueExpr.

Referenced by checkForImpliedValues(), klee::Executor::doImpliedValueConcretization(), and getImpliedValues().

Here is the call graph for this function:

Here is the caller graph for this function: