ExprUtil.h

Go to the documentation of this file.

//===-- ExprUtil.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_EXPRUTIL_H
#define KLEE_EXPRUTIL_H
 
#include "klee/Expr/ExprVisitor.h"
 
#include <vector>
 
namespace klee {
  class Array;
  class Expr;
  class ReadExpr;
  template<typename T> class ref;
 
  void findReads(ref<Expr> e, 
                 bool visitUpdates,
                 std::vector< ref<ReadExpr> > &result);
  
  void findSymbolicObjects(ref<Expr> e,
                           std::vector<const Array*> &results);
 
  template<typename InputIterator>
  void findSymbolicObjects(InputIterator begin, 
                           InputIterator end,
                           std::vector<const Array*> &results);
 
  class ConstantArrayFinder : public ExprVisitor {
  protected:
    ExprVisitor::Action visitRead(const ReadExpr &re);
 
  public:
    std::set<const Array *> results;
  };
}
 
#endif /* KLEE_EXPRUTIL_H */