Expr.h File Reference

#include "Machine.h"
#include "klee/util/Bits.h"
#include "klee/util/Ref.h"
#include "llvm/ADT/SmallVector.h"
#include "llvm/Support/Streams.h"
#include <set>
#include <vector>

Include dependency graph for Expr.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	klee::Expr
	Class representing symbolic expressions. More...
struct	klee::Expr::Expr::CreateArg
class	klee::ConstantExpr
class	klee::BinaryExpr
class	klee::CmpExpr
class	klee::NotOptimizedExpr
class	klee::UpdateNode
	Class representing a byte update of an array. More...
class	klee::Array
class	klee::UpdateList
	Class representing a complete list of updates into an array. More...
class	klee::ReadExpr
	Class representing a one byte read from an array. More...
class	klee::SelectExpr
	Class representing an if-then-else expression. More...
class	klee::ConcatExpr
class	klee::ExtractExpr
class	klee::CastExpr
Namespaces
namespace	llvm
namespace	klee
Defines
#define	CAST_EXPR_CLASS(_class_kind)
#define	ARITHMETIC_EXPR_CLASS(_class_kind)
#define	COMPARISON_EXPR_CLASS(_class_kind)
Functions
bool	klee::operator== (const Expr &lhs, const Expr &rhs)
bool	klee::operator< (const Expr &lhs, const Expr &rhs)
bool	klee::operator!= (const Expr &lhs, const Expr &rhs)
bool	klee::operator> (const Expr &lhs, const Expr &rhs)
bool	klee::operator<= (const Expr &lhs, const Expr &rhs)
bool	klee::operator>= (const Expr &lhs, const Expr &rhs)
std::ostream &	klee::operator<< (std::ostream &os, const Expr &e)
std::ostream &	klee::operator<< (std::ostream &os, const Expr::Kind kind)

---

Define Documentation

#define ARITHMETIC_EXPR_CLASS

(

_class_kind

)

Value:

class _class_kind ## Expr : public BinaryExpr {                      \
public:                                                              \
  static const Kind kind = _class_kind;                              \
  static const unsigned numKids = 2;                                 \
public:                                                              \
    _class_kind ## Expr(const ref<Expr> &l,                          \
                        const ref<Expr> &r) : BinaryExpr(l,r) {}     \
    static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) { \
      ref<Expr> res(new _class_kind ## Expr (l, r));                 \
      res->computeHash();                                            \
      return res;                                                    \
    }                                                                \
    static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r); \
    Width getWidth() const { return left->getWidth(); }              \
    Kind getKind() const { return _class_kind; }                     \
    virtual ref<Expr> rebuild(ref<Expr> kids[]) const {              \
      return create(kids[0], kids[1]);                               \
    }                                                                \
                                                                     \
    static bool classof(const Expr *E) {                             \
      return E->getKind() == Expr::_class_kind;                      \
    }                                                                \
    static bool classof(const  _class_kind ## Expr *) {              \
      return true;                                                   \
    }                                                                \
};                                                                   \

Definition at line 813 of file Expr.h.

#define CAST_EXPR_CLASS

(

_class_kind

)

Value:

class _class_kind ## Expr : public CastExpr {                    \
public:                                                          \
  static const Kind kind = _class_kind;                          \
  static const unsigned numKids = 1;                             \
public:                                                          \
    _class_kind ## Expr(ref<Expr> e, Width w) : CastExpr(e,w) {} \
    static ref<Expr> alloc(const ref<Expr> &e, Width w) {        \
      ref<Expr> r(new _class_kind ## Expr(e, w));                \
      r->computeHash();                                          \
      return r;                                                  \
    }                                                            \
    static ref<Expr> create(const ref<Expr> &e, Width w);        \
    Kind getKind() const { return _class_kind; }                 \
    virtual ref<Expr> rebuild(ref<Expr> kids[]) const {          \
      return create(kids[0], width);                             \
    }                                                            \
                                                                 \
    static bool classof(const Expr *E) {                         \
      return E->getKind() == Expr::_class_kind;                  \
    }                                                            \
    static bool classof(const  _class_kind ## Expr *) {          \
      return true;                                               \
    }                                                            \
};                                                               \

Definition at line 782 of file Expr.h.

#define COMPARISON_EXPR_CLASS

(

_class_kind

)

Value:

class _class_kind ## Expr : public CmpExpr {                         \
public:                                                              \
  static const Kind kind = _class_kind;                              \
  static const unsigned numKids = 2;                                 \
public:                                                              \
    _class_kind ## Expr(const ref<Expr> &l,                          \
                        const ref<Expr> &r) : CmpExpr(l,r) {}        \
    static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) { \
      ref<Expr> res(new _class_kind ## Expr (l, r));                 \
      res->computeHash();                                            \
      return res;                                                    \
    }                                                                \
    static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r); \
    Kind getKind() const { return _class_kind; }                     \
    virtual ref<Expr> rebuild(ref<Expr> kids[]) const {              \
      return create(kids[0], kids[1]);                               \
    }                                                                \
                                                                     \
    static bool classof(const Expr *E) {                             \
      return E->getKind() == Expr::_class_kind;                      \
    }                                                                \
    static bool classof(const  _class_kind ## Expr *) {              \
      return true;                                                   \
    }                                                                \
};                                                                   \

Definition at line 857 of file Expr.h.