blob: e0368203984807ad21564f2c3bc983fb6b212223 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
|
//===-- 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() {}
/// getInitialValue - Return the initial value for a symbolic byte.
///
/// This will only be called for constant arrays if the index is
/// out-of-bounds. If the value is unknown then the user should return a
/// ReadExpr at the initial version of this array.
virtual ref<Expr> getInitialValue(const Array& os, unsigned index) = 0;
};
}
#endif /* KLEE_EXPREVALUATOR_H */
|
