blob: 6bdb6c66d27b7802d6e68eb2484d851d79ae309a (
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
|
//===-- ImpliedValue.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_IMPLIEDVALUE_H
#define KLEE_IMPLIEDVALUE_H
#include "klee/Expr.h"
#include <vector>
// The idea of implied values is that often we know the result of some
// expression e is a concrete value C. In many cases this directly
// implies that some variable x embedded in e is also a concrete value
// (derived from C). This module is used for finding such variables
// and their computed values.
namespace klee {
class ConstantExpr;
class Expr;
class ReadExpr;
class Solver;
typedef std::vector< std::pair<ref<ReadExpr>,
ref<ConstantExpr> > > ImpliedValueList;
namespace ImpliedValue {
void getImpliedValues(ref<Expr> e, ref<ConstantExpr> cvalue,
ImpliedValueList &result);
void checkForImpliedValues(Solver *S, ref<Expr> e,
ref<ConstantExpr> cvalue);
}
}
#endif
|
