klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Solver.cpp File Reference
#include "klee/Solver.h"
#include "klee/SolverImpl.h"
#include "SolverStats.h"
#include "STPBuilder.h"
#include "MetaSMTBuilder.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 "klee/CommandLine.h"
#include <cassert>
#include <cstdio>
#include <map>
#include <vector>
#include <errno.h>
#include <unistd.h>
#include <signal.h>
#include <sys/wait.h>
#include <sys/ipc.h>
#include <sys/shm.h>
#include "llvm/Support/CommandLine.h"
Include dependency graph for Solver.cpp:

Go to the source code of this file.

Classes

class  ValidatingSolver
 
class  DummySolverImpl
 
class  STPSolverImpl
 

Macros

#define vc_bvBoolExtract   IAMTHESPAWNOFSATAN
 

Functions

llvm::cl::opt< bool > IgnoreSolverFailures ("ignore-solver-failures", llvm::cl::init(false), llvm::cl::desc("Ignore any solver failures (default=off)"))
 
static void stp_error_handler (const char *err_msg)
 
static SolverImpl::SolverRunStatus 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 SolverImpl::SolverRunStatus 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
 

Macro Definition Documentation

#define vc_bvBoolExtract   IAMTHESPAWNOFSATAN

Definition at line 26 of file Solver.cpp.

Function Documentation

llvm::cl::opt<bool> IgnoreSolverFailures ( "ignore-solver-failures"  ,
llvm::cl::  initfalse,
llvm::cl::  desc"Ignore any solver failures (default=off)" 
)

Referenced by runAndGetCexForked().

Here is the caller graph for this function:

static SolverImpl::SolverRunStatus 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 630 of file Solver.cpp.

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

Referenced by STPSolverImpl::computeInitialValues().

Here is the call graph for this function:

Here is the caller graph for this function:

static SolverImpl::SolverRunStatus 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
static void stp_error_handler ( const char *  err_msg)
static

Definition at line 523 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 664 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 521 of file Solver.cpp.

Referenced by STPSolverImpl::STPSolverImpl().

unsigned char* shared_memory_ptr
static

Definition at line 519 of file Solver.cpp.

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

const unsigned shared_memory_size = 1<<20
static

Definition at line 520 of file Solver.cpp.

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