Expr.h File Reference

#include "klee/ADT/Bits.h"
#include "klee/ADT/Ref.h"
#include "llvm/ADT/APFloat.h"
#include "llvm/ADT/APInt.h"
#include "llvm/ADT/DenseSet.h"
#include "llvm/ADT/SmallVector.h"
#include "llvm/Support/CommandLine.h"
#include "llvm/Support/raw_ostream.h"
#include <sstream>
#include <set>
#include <vector>
#include <map>

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::CreateArg
class	klee::NonConstantExpr
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::NotExpr
class	klee::CastExpr
class	klee::ConstantExpr

Namespaces
namespace	llvm
namespace	klee

Macros
#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)
llvm::raw_ostream &	klee::operator<< (llvm::raw_ostream &os, const Expr &e)
llvm::raw_ostream &	klee::operator<< (llvm::raw_ostream &os, const Expr::Kind kind)
std::stringstream &	klee::operator<< (std::stringstream &os, const Expr &e)
std::stringstream &	klee::operator<< (std::stringstream &os, const Expr::Kind kind)

Variables
llvm::cl::OptionCategory	klee::ExprCat

Macro Definition Documentation

ARITHMETIC_EXPR_CLASS

#define ARITHMETIC_EXPR_CLASS

(

_class_kind

)

Definition at line 902 of file Expr.h.

CAST_EXPR_CLASS

#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 871 of file Expr.h.

COMPARISON_EXPR_CLASS

#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; }            \
                                                                               \
  protected:                                                                   \
    virtual int compareContents(const Expr &b) const {                         \
      /* No attributes to compare. */                                          \
      return 0;                                                                \
    }                                                                          \
  };

Definition at line 951 of file Expr.h.