about summary refs log tree commit diff homepage
path: root/include/klee/Support
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2020-04-03 18:57:53 +0100
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2020-04-30 09:25:36 +0100
commit02fed84be089d81a5a9a812c2c8dd112f5e2fa71 (patch)
tree749c6030b8e371dbfd10906f13374d55a84be6d2 /include/klee/Support
parente2cbdaeb98168db12aba4abab04eea2416c0931c (diff)
downloadklee-02fed84be089d81a5a9a812c2c8dd112f5e2fa71.tar.gz
Removed include/klee/util and moved header files to appropriate places
Diffstat (limited to 'include/klee/Support')
-rw-r--r--include/klee/Support/FloatEvaluation.h5
-rw-r--r--include/klee/Support/IntEvaluation.h2
-rw-r--r--include/klee/Support/PrintContext.h102
3 files changed, 106 insertions, 3 deletions
diff --git a/include/klee/Support/FloatEvaluation.h b/include/klee/Support/FloatEvaluation.h
index 37392576..d6fcc73c 100644
--- a/include/klee/Support/FloatEvaluation.h
+++ b/include/klee/Support/FloatEvaluation.h
@@ -12,8 +12,9 @@
 #ifndef KLEE_FLOATEVALUATION_H
 #define KLEE_FLOATEVALUATION_H
 
-#include "klee/util/Bits.h"     //bits64::truncateToNBits
-#include "IntEvaluation.h" //ints::sext
+#include "IntEvaluation.h" // ints::sext
+
+#include "klee/ADT/Bits.h" // bits64::truncateToNBits
 
 #include "llvm/Support/ErrorHandling.h"
 #include "llvm/Support/MathExtras.h"
diff --git a/include/klee/Support/IntEvaluation.h b/include/klee/Support/IntEvaluation.h
index 27a8daf0..0e9a40d6 100644
--- a/include/klee/Support/IntEvaluation.h
+++ b/include/klee/Support/IntEvaluation.h
@@ -10,7 +10,7 @@
 #ifndef KLEE_INTEVALUATION_H
 #define KLEE_INTEVALUATION_H
 
-#include "klee/util/Bits.h"
+#include "klee/ADT/Bits.h"
 
 #define MAX_BITS (sizeof(uint64_t) * 8)
 
diff --git a/include/klee/Support/PrintContext.h b/include/klee/Support/PrintContext.h
new file mode 100644
index 00000000..de9094da
--- /dev/null
+++ b/include/klee/Support/PrintContext.h
@@ -0,0 +1,102 @@
+//===-- PrintContext.h ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_PRINTCONTEXT_H
+#define KLEE_PRINTCONTEXT_H
+
+#include "klee/Expr/Expr.h"
+
+#include "llvm/Support/raw_ostream.h"
+
+#include <sstream>
+#include <string>
+#include <stack>
+
+/// PrintContext - Helper class for pretty printing.
+/// It provides a basic wrapper around llvm::raw_ostream that keeps track of
+/// how many characters have been used on the current line.
+///
+/// It also provides an optional way keeping track of the various levels of indentation
+/// by using a stack.
+/// \sa breakLineI() , \sa pushIndent(), \sa popIndent()
+class PrintContext {
+private:
+  llvm::raw_ostream &os;
+  std::string newline;
+
+  ///This is used to keep track of the stack of indentations used by
+  /// \sa breakLineI()
+  /// \sa pushIndent()
+  /// \sa popIndent()
+  std::stack<unsigned int> indentStack;
+
+public:
+  /// Number of characters on the current line.
+  unsigned pos;
+
+  PrintContext(llvm::raw_ostream &_os) : os(_os), newline("\n"), indentStack(), pos()
+  {
+	  indentStack.push(pos);
+  }
+
+  void setNewline(const std::string &_newline) {
+    newline = _newline;
+  }
+
+  void breakLine(unsigned indent=0) {
+    os << newline;
+    if (indent)
+      os.indent(indent) << ' ';
+    pos = indent;
+  }
+
+  ///Break line using the indent on the top of the indent stack
+  /// \return The PrintContext object so the method is chainable
+  PrintContext& breakLineI()
+  {
+	  breakLine(indentStack.top());
+	  return *this;
+  }
+
+  ///Add the current position on the line to the top of the indent stack
+  /// \return The PrintContext object so the method is chainable
+  PrintContext& pushIndent()
+  {
+	  indentStack.push(pos);
+	  return *this;
+  }
+
+  ///Pop the top off the indent stack
+  /// \return The PrintContext object so the method is chainable
+  PrintContext& popIndent()
+  {
+	  indentStack.pop();
+	  return *this;
+  }
+
+  /// write - Output a string to the stream and update the
+  /// position. The stream should not have any newlines.
+  void write(const std::string &s) {
+    os << s;
+    pos += s.length();
+  }
+
+  template <typename T>
+  PrintContext &operator<<(T elt) {
+    std::string str;
+    llvm::raw_string_ostream ss(str);
+    ss << elt;
+    write(ss.str());
+    return *this;
+  }
+
+};
+
+
+#endif /* KLEE_PRINTCONTEXT_H */