Expr::print shouldn't introduce line breaks or extra formatting.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72921 91177308-0d34-0410-b5e6-96231b3b80d8

3 files changed, 22 insertions, 3 deletions

diff --git a/include/klee/util/ExprPPrinter.h b/include/klee/util/ExprPPrinter.h
index a1961e2b..63e6611d 100644
--- a/include/klee/util/ExprPPrinter.h
+++ b/include/klee/util/ExprPPrinter.h
@@ -42,9 +42,20 @@ namespace klee {
         scan(*it);
     }
 
+    /// printOne - Pretty print a single expression prefixed by a
+    /// message and followed by a line break.
     static void printOne(std::ostream &os, const char *message, 
                          const ref<Expr> &e);
 
+    /// printSingleExpr - Pretty print a single expression.
+    ///
+    /// The expression will not be followed by a line break.
+    ///
+    /// Note that if the output stream is not positioned at the
+    /// beginning of a line then printing will not resume at the
+    /// correct position following any output line breaks.
+    static void printSingleExpr(std::ostream &os, const ref<Expr> &e);
+
     static void printConstraints(std::ostream &os,
                                  const ConstraintManager &constraints);
 
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index bc871808..d58c9085 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -320,8 +320,7 @@ ref<Expr> Expr::createPointer(uint64_t v) {
 }
 
 void Expr::print(std::ostream &os) const {
-  const ref<Expr> tmp((Expr*)this);
-  ExprPPrinter::printOne(os, "", tmp);
+  ExprPPrinter::printSingleExpr(os, (Expr*)this);
 }
 
 /***/
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index 94c0ac17..c27e265e 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -406,7 +406,6 @@ public:
             PC << "(Not";
             printWidth(PC, e);
             PC << ' ';
-            // FIXME: This is a boom if right is a constant.
             print(ee->right, PC);
             PC << ')';
             return;
@@ -484,6 +483,16 @@ void ExprPPrinter::printOne(std::ostream &os,
   PC.breakLine();
 }
 
+void ExprPPrinter::printSingleExpr(std::ostream &os, const ref<Expr> &e) {
+  PPrinter p(os);
+  p.scan(e);
+
+  // FIXME: Need to figure out what to do here. Probably print as a
+  // "forward declaration" with whatever syntax we pick for that.
+  PrintContext PC(os);
+  p.print(e, PC);
+}
+
 void ExprPPrinter::printConstraints(std::ostream &os,
                                     const ConstraintManager &constraints) {
   printQuery(os, constraints, ConstantExpr::alloc(false, Expr::Bool));