1 //===-- ExprUtil.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_EXPRUTIL_H 11 #define KLEE_EXPRUTIL_H 12 13 #include "klee/Expr/ExprVisitor.h" 14 15 #include <vector> 16 17 namespace klee { 18 class Array; 19 class Expr; 20 class ReadExpr; 21 template<typename T> class ref; 22 23 /// Find all ReadExprs used in the expression DAG. If visitUpdates 24 /// is true then this will including those reachable by traversing 25 /// update lists. Note that this may be slow and return a large 26 /// number of results. 27 void findReads(ref<Expr> e, 28 bool visitUpdates, 29 std::vector< ref<ReadExpr> > &result); 30 31 /// Return a list of all unique symbolic objects referenced by the given 32 /// expression. 33 void findSymbolicObjects(ref<Expr> e, 34 std::vector<const Array*> &results); 35 36 /// Return a list of all unique symbolic objects referenced by the 37 /// given expression range. 38 template<typename InputIterator> 39 void findSymbolicObjects(InputIterator begin, 40 InputIterator end, 41 std::vector<const Array*> &results); 42 43 class ConstantArrayFinder : public ExprVisitor { 44 protected: 45 ExprVisitor::Action visitRead(const ReadExpr &re); 46 47 public: 48 std::set<const Array *> results; 49 }; 50 } 51 52 #endif /* KLEE_EXPRUTIL_H */ 53