klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ImpliedValue.h
Go to the documentation of this file.
1 //===-- ImpliedValue.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_IMPLIEDVALUE_H
11 #define KLEE_IMPLIEDVALUE_H
12 
13 #include "klee/Expr.h"
14 
15 #include <vector>
16 
17 // The idea of implied values is that often we know the result of some
18 // expression e is a concrete value C. In many cases this directly
19 // implies that some variable x embedded in e is also a concrete value
20 // (derived from C). This module is used for finding such variables
21 // and their computed values.
22 
23 namespace klee {
24  class ConstantExpr;
25  class Expr;
26  class ReadExpr;
27  class Solver;
28 
29  typedef std::vector< std::pair<ref<ReadExpr>,
31 
32  namespace ImpliedValue {
34  ImpliedValueList &result);
36  ref<ConstantExpr> cvalue);
37  }
38 
39 }
40 
41 #endif
void checkForImpliedValues(Solver *S, ref< Expr > e, ref< ConstantExpr > cvalue)
#define Expr
Definition: STPBuilder.h:19
std::vector< std::pair< ref< ReadExpr >, ref< ConstantExpr > > > ImpliedValueList
Definition: ImpliedValue.h:27
void getImpliedValues(ref< Expr > e, ref< ConstantExpr > cvalue, ImpliedValueList &result)