ExprEvaluator.h

Go to the documentation of this file.

//===-- ExprEvaluator.h -----------------------------------------*- C++ -*-===//
//
//                     The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
 
#ifndef KLEE_EXPREVALUATOR_H
#define KLEE_EXPREVALUATOR_H
 
#include "klee/Expr/Expr.h"
#include "klee/Expr/ExprVisitor.h"
 
namespace klee {
  class ExprEvaluator : public ExprVisitor {
  protected:
    Action evalRead(const UpdateList &ul, unsigned index);
    Action visitRead(const ReadExpr &re);
    Action visitExpr(const Expr &e);
      
    Action protectedDivOperation(const BinaryExpr &e);
    Action visitUDiv(const UDivExpr &e);
    Action visitSDiv(const SDivExpr &e);
    Action visitURem(const URemExpr &e);
    Action visitSRem(const SRemExpr &e);
    Action visitExprPost(const Expr& e);
      
  public:
    ExprEvaluator() {}
 
    virtual ref<Expr> getInitialValue(const Array& os, unsigned index) = 0;
  };
}
 
#endif /* KLEE_EXPREVALUATOR_H */