diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-04-03 18:57:53 +0100 |
---|---|---|
committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2020-04-30 09:25:36 +0100 |
commit | 02fed84be089d81a5a9a812c2c8dd112f5e2fa71 (patch) | |
tree | 749c6030b8e371dbfd10906f13374d55a84be6d2 /include/klee/Support | |
parent | e2cbdaeb98168db12aba4abab04eea2416c0931c (diff) | |
download | klee-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.h | 5 | ||||
-rw-r--r-- | include/klee/Support/IntEvaluation.h | 2 | ||||
-rw-r--r-- | include/klee/Support/PrintContext.h | 102 |
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 */ |