klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
STPBuilder.cpp File Reference
#include "STPBuilder.h"
#include "klee/Expr.h"
#include "klee/Solver.h"
#include "klee/util/Bits.h"
#include "ConstantDivision.h"
#include "SolverStats.h"
#include "llvm/Support/CommandLine.h"
#include <cstdio>
#include <algorithm>
#include <cassert>
#include <map>
#include <sstream>
#include <vector>
Include dependency graph for STPBuilder.cpp:

Go to the source code of this file.

Macros

#define vc_bvBoolExtract   IAMTHESPAWNOFSATAN
 
#define vc_bvLeftShiftExpr   IAMTHESPAWNOFSATAN
 
#define vc_bvRightShiftExpr   IAMTHESPAWNOFSATAN
 
#define vc_bvVar32LeftShiftExpr   IAMTHESPAWNOFSATAN
 
#define vc_bvVar32RightShiftExpr   IAMTHESPAWNOFSATAN
 
#define vc_bvVar32DivByPowOfTwoExpr   IAMTHESPAWNOFSATAN
 
#define vc_bvCreateMemoryArray   IAMTHESPAWNOFSATAN
 
#define vc_bvReadMemoryArray   IAMTHESPAWNOFSATAN
 
#define vc_bvWriteToMemoryArray   IAMTHESPAWNOFSATAN
 

Macro Definition Documentation

#define vc_bvBoolExtract   IAMTHESPAWNOFSATAN

Definition at line 23 of file STPBuilder.cpp.

#define vc_bvCreateMemoryArray   IAMTHESPAWNOFSATAN

Definition at line 31 of file STPBuilder.cpp.

#define vc_bvLeftShiftExpr   IAMTHESPAWNOFSATAN

Definition at line 25 of file STPBuilder.cpp.

#define vc_bvReadMemoryArray   IAMTHESPAWNOFSATAN

Definition at line 32 of file STPBuilder.cpp.

#define vc_bvRightShiftExpr   IAMTHESPAWNOFSATAN

Definition at line 26 of file STPBuilder.cpp.

#define vc_bvVar32DivByPowOfTwoExpr   IAMTHESPAWNOFSATAN

Definition at line 30 of file STPBuilder.cpp.

#define vc_bvVar32LeftShiftExpr   IAMTHESPAWNOFSATAN

Definition at line 28 of file STPBuilder.cpp.

#define vc_bvVar32RightShiftExpr   IAMTHESPAWNOFSATAN

Definition at line 29 of file STPBuilder.cpp.

#define vc_bvWriteToMemoryArray   IAMTHESPAWNOFSATAN

Definition at line 33 of file STPBuilder.cpp.