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