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 <iostream>
#include <map>
#include <sstream>
#include <vector>

Include dependency graph for STPBuilder.cpp:

Go to the source code of this file.

Defines
#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

---

Define 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.