about summary refs log tree commit diff homepage
path: root/lib/Expr/ExprPPrinter.cpp
diff options
context:
space:
mode:
authorDaniel Dunbar <daniel@zuster.org>2009-06-07 07:36:26 +0000
committerDaniel Dunbar <daniel@zuster.org>2009-06-07 07:36:26 +0000
commit24e065075e7ec973db84639725696b9f84975b2f (patch)
tree83d77fb2ea51bd12745567fbabc9c3b1936391d4 /lib/Expr/ExprPPrinter.cpp
parent98633b8240294910f74877e4c8b992bc5669ada1 (diff)
downloadklee-24e065075e7ec973db84639725696b9f84975b2f.tar.gz
Eliminate anonymous versions.
  - For now, this means the isRooted flag for arrays isn't propogated to the
    kquery language. We should figure out how to do this, but allow anonymous
    versions isn't the right way.

Also, improved the error on invalid writes a bit.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73018 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/Expr/ExprPPrinter.cpp')
-rw-r--r--lib/Expr/ExprPPrinter.cpp6
1 files changed, 4 insertions, 2 deletions
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index f8c6cabc..affde4ad 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -215,8 +215,10 @@ class PPrinter : public ExprPPrinter {
     if (openedList)
       PC << ']';
 
-    if (updates.isRooted)
-      PC << " @ arr" << updates.root->id;
+    // FIXME: Figure out how isRooted should be dealt with in the language. The
+    // old solution of using "anonymous" arrays is not a good idea.
+
+    PC << " @ arr" << updates.root->id;
   }
 
   void printWidth(PrintContext &PC, ref<Expr> e) {