about summary refs log tree commit diff homepage
path: root/include
diff options
context:
space:
mode:
Diffstat (limited to 'include')
-rw-r--r--include/klee/util/ExprPPrinter.h11
1 files changed, 11 insertions, 0 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);