9 files changed, 97 insertions, 1 deletions
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 0fb8f8db..b4ab8a1c 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -382,6 +382,19 @@ AC_SUBST(KLEE_BITCODE_C_COMPILER,$klee_llvm_bc_c_compiler)
 AC_SUBST(KLEE_BITCODE_CXX_COMPILER,$klee_llvm_bc_cxx_compiler)
 
 dnl **************************************************************************
+dnl User option to disable timestamping.
+
+AC_ARG_ENABLE([timestamp],AS_HELP_STRING([--enable-timestamp],
+	[Enable timestamping the source code while building. (default=disabled)]))
+
+if test "x${enable_timestamp}" = "xyes" ; then
+  AC_DEFINE(KLEE_ENABLE_TIMESTAMP,[1],[Enable time stamping the sources])
+  AC_MSG_NOTICE([Source timestamping enabled.])
+else
+  AC_MSG_NOTICE([Source timestamping disabled.])
+fi
+
+dnl **************************************************************************
 dnl User option to enable uClibc support.
 
 AC_ARG_WITH(uclibc,
diff --git a/configure b/configure
index f6059789..35ec06d1 100755
--- a/configure
+++ b/configure
@@ -735,6 +735,7 @@ enable_cxx11
 with_llvm_build_mode
 with_llvmcc
 with_llvmcxx
+enable_timestamp
 with_uclibc
 enable_posix_runtime
 with_runtime
@@ -1373,6 +1374,8 @@ Optional Features:
   --disable-FEATURE       do not include FEATURE (same as --enable-FEATURE=no)
   --enable-FEATURE[=ARG]  include FEATURE [ARG=yes]
   --enable-cxx11          Build using C++11
+  --enable-timestamp      Enable timestamping the source code while building.
+                          (default=disabled)
   --enable-posix-runtime  Enable the POSIX runtime
 
 Optional Packages:
@@ -3996,6 +3999,24 @@ KLEE_BITCODE_CXX_COMPILER=$klee_llvm_bc_cxx_compiler
 
 
 
+# Check whether --enable-timestamp was given.
+if test "${enable_timestamp+set}" = set; then :
+  enableval=$enable_timestamp;
+fi
+
+
+if test "x${enable_timestamp}" = "xyes" ; then
+
+$as_echo "#define KLEE_ENABLE_TIMESTAMP 1" >>confdefs.h
+
+  { $as_echo "$as_me:${as_lineno-$LINENO}: Source timestamping enabled." >&5
+$as_echo "$as_me: Source timestamping enabled." >&6;}
+else
+  { $as_echo "$as_me:${as_lineno-$LINENO}: Source timestamping disabled." >&5
+$as_echo "$as_me: Source timestamping disabled." >&6;}
+fi
+
+
 
 # Check whether --with-uclibc was given.
 if test "${with_uclibc+set}" = set; then :
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index 87d6ee75..76d391e4 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -72,6 +72,9 @@
 /* Define to 1 if you have the <zlib.h> header file. */
 #undef HAVE_ZLIB_H
 
+/* Enable time stamping the sources */
+#undef KLEE_ENABLE_TIMESTAMP
+
 /* Define to empty or 'const' depending on how SELinux qualifies its security
    context parameters. */
 #undef KLEE_SELINUX_CTX_CONST
diff --git a/include/klee/util/ExprEvaluator.h b/include/klee/util/ExprEvaluator.h
index 6b67a1cf..313ac0a5 100644
--- a/include/klee/util/ExprEvaluator.h
+++ b/include/klee/util/ExprEvaluator.h
@@ -25,6 +25,7 @@ namespace klee {
     Action visitSDiv(const SDivExpr &e);
     Action visitURem(const URemExpr &e);
     Action visitSRem(const SRemExpr &e);
+    Action visitExprPost(const Expr& e);
       
   public:
     ExprEvaluator() {}
diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp
index 1a146641..6b84cd6f 100644
--- a/lib/Expr/ExprEvaluator.cpp
+++ b/lib/Expr/ExprEvaluator.cpp
@@ -97,3 +97,12 @@ ExprVisitor::Action ExprEvaluator::visitURem(const URemExpr &e) {
 ExprVisitor::Action ExprEvaluator::visitSRem(const SRemExpr &e) { 
   return protectedDivOperation(e); 
 }
+
+ExprVisitor::Action ExprEvaluator::visitExprPost(const Expr& e) {
+  // When evaluating an assignment we should fold NotOptimizedExpr
+  // nodes so we can fully evaluate.
+  if (e.getKind() == Expr::NotOptimized) {
+    return Action::changeTo(static_cast<const NotOptimizedExpr&>(e).src);
+  }
+  return Action::skipChildren();
+}
diff --git a/lib/Support/PrintVersion.cpp b/lib/Support/PrintVersion.cpp
index b4ff9811..dfea5007 100644
--- a/lib/Support/PrintVersion.cpp
+++ b/lib/Support/PrintVersion.cpp
@@ -17,7 +17,9 @@
 void klee::printVersion()
 {
   llvm::outs() << PACKAGE_STRING " (" PACKAGE_URL ")\n";
+#ifdef KLEE_ENABLE_TIMESTAMP
   llvm::outs() << "  Built " __DATE__ " (" __TIME__ ")\n";
+#endif
   llvm::outs() << "  Build mode: " << KLEE_BUILD_MODE "\n";
   llvm::outs() << "  Build revision: ";
 #ifdef KLEE_BUILD_REVISION
diff --git a/unittests/Assignment/AssignmentTest.cpp b/unittests/Assignment/AssignmentTest.cpp
new file mode 100644
index 00000000..0eaa28f1
--- /dev/null
+++ b/unittests/Assignment/AssignmentTest.cpp
@@ -0,0 +1,35 @@
+#include "klee/util/ArrayCache.h"
+#include "klee/util/Assignment.h"
+#include "gtest/gtest.h"
+#include <iostream>
+#include <vector>
+
+int finished = 0;
+
+using namespace klee;
+
+TEST(AssignmentTest, FoldNotOptimized)
+{
+  ArrayCache ac;
+  const Array* array = ac.CreateArray("simple_array", /*size=*/ 1);
+  // Create a simple assignment
+  std::vector<const Array*> objects;
+  std::vector<unsigned char> value;
+  std::vector< std::vector<unsigned char> > values;
+  objects.push_back(array);
+  value.push_back(128);
+  values.push_back(value);
+  // We want to simplify to a constant so allow free values so
+  // if the assignment is incomplete we don't get back a constant.
+  Assignment assignment(objects, values, /*_allowFreeValues=*/true);
+
+  // Now make an expression that reads from the array at position
+  // zero.
+  ref<Expr> read = NotOptimizedExpr::alloc(Expr::createTempRead(array, Expr::Int8));
+
+  // Now evaluate. The OptimizedExpr should be folded
+  ref<Expr> evaluated = assignment.evaluate(read);
+  const ConstantExpr* asConstant = dyn_cast<ConstantExpr>(evaluated);
+  ASSERT_TRUE(asConstant != NULL);
+  ASSERT_EQ(asConstant->getZExtValue(), (unsigned) 128);
+}
diff --git a/unittests/Assignment/Makefile b/unittests/Assignment/Makefile
new file mode 100644
index 00000000..d4110c80
--- /dev/null
+++ b/unittests/Assignment/Makefile
@@ -0,0 +1,12 @@
+##===- unittests/Assignment/Makefile -----------------------*- Makefile -*-===##
+
+LEVEL := ../..
+include $(LEVEL)/Makefile.config
+
+TESTNAME := Assignment
+USEDLIBS := kleaverExpr.a
+LINK_COMPONENTS := support
+
+include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
+
+CXXFLAGS += -DLLVM_29_UNITTEST
diff --git a/unittests/Makefile b/unittests/Makefile
index b7e51371..2a73b809 100644
--- a/unittests/Makefile
+++ b/unittests/Makefile
@@ -17,7 +17,7 @@ CPP.Flags += -I$(LLVM_SRC_ROOT)/utils/unittest/googletest/include/
 CPP.Flags += -Wno-variadic-macros
 
 # FIXME: Parallel dirs is broken?
-DIRS = Expr Solver Ref
+DIRS = Expr Solver Ref Assignment
 
 include $(LEVEL)/Makefile.common