Solver.cpp File Reference

#include "klee/Solver.h"
#include "klee/SolverImpl.h"
#include "SolverStats.h"
#include "STPBuilder.h"
#include "klee/Constraints.h"
#include "klee/Expr.h"
#include "klee/TimerStatIncrementer.h"
#include "klee/util/Assignment.h"
#include "klee/util/ExprPPrinter.h"
#include "klee/util/ExprUtil.h"
#include "klee/Internal/Support/Timer.h"
#include <cassert>
#include <cstdio>
#include <map>
#include <vector>
#include <signal.h>
#include <sys/wait.h>
#include <sys/ipc.h>
#include <sys/shm.h>

Include dependency graph for Solver.cpp:

Go to the source code of this file.

Classes
class	ValidatingSolver
class	STPSolverImpl
Defines
#define	vc_bvBoolExtract   IAMTHESPAWNOFSATAN
Functions
static void	stp_error_handler (const char *err_msg)
static void	runAndGetCex (::VC vc, STPBuilder *builder,::VCExpr q, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)
static void	stpTimeoutHandler (int x)
static bool	runAndGetCexForked (::VC vc, STPBuilder *builder,::VCExpr q, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution, double timeout)
Variables
static unsigned char *	shared_memory_ptr
static const unsigned	shared_memory_size = 1<<20
static int	shared_memory_id

---

Define Documentation

#define vc_bvBoolExtract   IAMTHESPAWNOFSATAN

Definition at line 24 of file Solver.cpp.

---

Function Documentation

static void runAndGetCex	(	::VC	vc,
		STPBuilder *	builder,
		::VCExpr	q,
		const std::vector< const Array * > &	objects,
		std::vector< std::vector< unsigned char > > &	values,
		bool &	hasSolution
	)			[static]

Definition at line 505 of file Solver.cpp.

References klee::STPBuilder::getInitialRead(), and klee::Array::size.

Referenced by STPSolverImpl::computeInitialValues().

Here is the call graph for this function:

Here is the caller graph for this function:

static bool runAndGetCexForked	(	::VC	vc,
		STPBuilder *	builder,
		::VCExpr	q,
		const std::vector< const Array * > &	objects,
		std::vector< std::vector< unsigned char > > &	values,
		bool &	hasSolution,
		double	timeout
	)			[static]

Definition at line 536 of file Solver.cpp.

References klee::STPBuilder::getInitialRead(), shared_memory_ptr, shared_memory_size, klee::Array::size, and stpTimeoutHandler().

Referenced by STPSolverImpl::computeInitialValues().

Here is the call graph for this function:

Here is the caller graph for this function:

static void stp_error_handler

(

const char *

err_msg

)

[static]

Definition at line 406 of file Solver.cpp.

Referenced by STPSolverImpl::STPSolverImpl().

Here is the caller graph for this function:

static void stpTimeoutHandler

(

int

x

)

[static]

Definition at line 532 of file Solver.cpp.

Referenced by runAndGetCexForked().

Here is the caller graph for this function:

---

Variable Documentation

int shared_memory_id [static]

Definition at line 404 of file Solver.cpp.

Referenced by STPSolverImpl::STPSolverImpl().

unsigned char* shared_memory_ptr [static]

Definition at line 402 of file Solver.cpp.

Referenced by runAndGetCexForked(), and STPSolverImpl::STPSolverImpl().

const unsigned shared_memory_size = 1<<20 [static]

Definition at line 403 of file Solver.cpp.

Referenced by runAndGetCexForked(), and STPSolverImpl::STPSolverImpl().