klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExprEvaluator.h
Go to the documentation of this file.
1 //===-- ExprEvaluator.h -----------------------------------------*- C++ -*-===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #ifndef KLEE_EXPREVALUATOR_H
11 #define KLEE_EXPREVALUATOR_H
12 
13 #include "klee/Expr.h"
14 #include "klee/util/ExprVisitor.h"
15 
16 namespace klee {
17  class ExprEvaluator : public ExprVisitor {
18  protected:
19  Action evalRead(const UpdateList &ul, unsigned index);
20  Action visitRead(const ReadExpr &re);
21  Action visitExpr(const Expr &e);
22 
24  Action visitUDiv(const UDivExpr &e);
25  Action visitSDiv(const SDivExpr &e);
26  Action visitURem(const URemExpr &e);
27  Action visitSRem(const SRemExpr &e);
28 
29  public:
31 
37  virtual ref<Expr> getInitialValue(const Array& os, unsigned index) = 0;
38  };
39 }
40 
41 #endif
Action visitSRem(const SRemExpr &e)
Action visitExpr(const Expr &e)
Class representing a complete list of updates into an array.
Definition: Expr.h:655
Class representing symbolic expressions.
Definition: Expr.h:88
Action visitURem(const URemExpr &e)
Action protectedDivOperation(const BinaryExpr &e)
Action visitRead(const ReadExpr &re)
Action visitSDiv(const SDivExpr &e)
Action evalRead(const UpdateList &ul, unsigned index)
virtual ref< Expr > getInitialValue(const Array &os, unsigned index)=0
Action visitUDiv(const UDivExpr &e)
Class representing a one byte read from an array.
Definition: Expr.h:681