1 files changed, 59 insertions, 0 deletions
diff --git a/lib/Expr/AssignmentGenerator.h b/lib/Expr/AssignmentGenerator.h
new file mode 100644
index 00000000..fea1168a
--- /dev/null
+++ b/lib/Expr/AssignmentGenerator.h
@@ -0,0 +1,59 @@
+//===-- AssignmentGenerator.h ---------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_ASSIGNMENTGENERATOR_H
+#define KLEE_ASSIGNMENTGENERATOR_H
+
+#include <vector>
+
+#include "klee/Expr.h"
+#include "klee/util/Ref.h"
+
+namespace klee {
+class Assignment;
+} /* namespace klee */
+
+namespace klee {
+
+class Expr;
+template <class T> class ref;
+
+class AssignmentGenerator {
+public:
+  static bool generatePartialAssignment(const ref<Expr> &e, ref<Expr> &val,
+                                        Assignment *&a);
+
+private:
+  static bool helperGenerateAssignment(const ref<Expr> &e, ref<Expr> &val,
+                                       Assignment *&a, Expr::Width width,
+                                       bool sign);
+
+  static bool isReadExprAtOffset(ref<Expr> e, const ReadExpr *base,
+                                 ref<Expr> offset);
+  static ReadExpr *hasOrderedReads(ref<Expr> e);
+
+  static ref<Expr> createSubExpr(const ref<Expr> &l, ref<Expr> &r);
+  static ref<Expr> createAddExpr(const ref<Expr> &l, ref<Expr> &r);
+  static ref<Expr> createMulExpr(const ref<Expr> &l, ref<Expr> &r);
+  static ref<Expr> createDivExpr(const ref<Expr> &l, ref<Expr> &r, bool sign);
+  static ref<Expr> createDivRem(const ref<Expr> &l, ref<Expr> &r, bool sign);
+  static ref<Expr> createShlExpr(const ref<Expr> &l, ref<Expr> &r);
+  static ref<Expr> createLShrExpr(const ref<Expr> &l, ref<Expr> &r);
+  static ref<Expr> createAndExpr(const ref<Expr> &l, ref<Expr> &r);
+  static ref<Expr> createExtractExpr(const ref<Expr> &l, ref<Expr> &r);
+  static ref<Expr> createExtendExpr(const ref<Expr> &l, ref<Expr> &r);
+
+  static std::vector<unsigned char> getByteValue(ref<Expr> &val);
+  static std::vector<unsigned char>
+  getIndexedValue(const std::vector<unsigned char> &c_val, ConstantExpr &index,
+                  const unsigned int size);
+};
+} // namespace klee
+
+#endif