diff options
author | Andrea Mattavelli <andreamattavelli@users.noreply.github.com> | 2017-07-20 07:32:59 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-07-20 07:32:59 +0100 |
commit | fbbf33a251b57cf73398d06fa3533c1ed7774055 (patch) | |
tree | c583f7f13f92f08086a7b72c78a87ea28394f07f /lib/Support/TreeStream.cpp | |
parent | cc1a60141d01cf13a222db05e18f29f9bda40921 (diff) | |
parent | 7aa7f0aaebca40288c5dee038cf7bc84bf1462a4 (diff) | |
download | klee-fbbf33a251b57cf73398d06fa3533c1ed7774055.tar.gz |
Merge pull request #704 from ccadar/TreeStream
Fixes bug in TreeStreamWriter::write reported by @gladtbx in #562. A…
Diffstat (limited to 'lib/Support/TreeStream.cpp')
-rw-r--r-- | lib/Support/TreeStream.cpp | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/lib/Support/TreeStream.cpp b/lib/Support/TreeStream.cpp index ef59b2a9..a0e1596f 100644 --- a/lib/Support/TreeStream.cpp +++ b/lib/Support/TreeStream.cpp @@ -63,7 +63,6 @@ TreeOStream TreeStreamWriter::open(const TreeOStream &os) { } void TreeStreamWriter::write(TreeOStream &os, const char *s, unsigned size) { -#if 1 if (bufferCount && (os.id!=lastID || size+bufferCount>bufferSize)) flushBuffer(); @@ -77,13 +76,8 @@ void TreeStreamWriter::write(TreeOStream &os, const char *s, unsigned size) { } else { output->write(reinterpret_cast<const char*>(&os.id), 4); output->write(reinterpret_cast<const char*>(&size), 4); - output->write(buffer, size); + output->write(s, size); } -#else - output->write(reinterpret_cast<const char*>(&os.id), 4); - output->write(reinterpret_cast<const char*>(&size), 4); - output->write(s, size); -#endif } void TreeStreamWriter::flushBuffer() { |