Restoring ostream format. Resolves a few CIDs 1362780. (#1543)

5 files changed, 87 insertions, 1 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 33218dbe9..ddee2e72b 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -38,6 +38,8 @@ libutil_la_SOURCES = \
 	index.h \
 	maybe.h \
 	ntuple.h \
+	ostream_util.cpp \
+	ostream_util.h \
 	proof.h \
 	regexp.cpp \
 	regexp.h \
diff --git a/src/util/ostream_util.cpp b/src/util/ostream_util.cpp
new file mode 100644
index 000000000..3d6eeea01
--- /dev/null
+++ b/src/util/ostream_util.cpp
@@ -0,0 +1,31 @@
+/*********************                                                        */
+/*! \file result.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Tim King, Morgan Deters, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utilities for using ostreams.
+ **
+ ** Utilities for using ostreams.
+ **/
+#include "util/ostream_util.h"
+
+namespace CVC4 {
+
+StreamFormatScope::StreamFormatScope(std::ostream& out)
+    : d_out(out), d_format_flags(out.flags()), d_precision(out.precision())
+{
+}
+
+StreamFormatScope::~StreamFormatScope()
+{
+  d_out.precision(d_precision);
+  d_out.flags(d_format_flags);
+}
+
+}  // namespace CVC4
diff --git a/src/util/ostream_util.h b/src/util/ostream_util.h
new file mode 100644
index 000000000..e047caa17
--- /dev/null
+++ b/src/util/ostream_util.h
@@ -0,0 +1,49 @@
+/*********************                                                        */
+/*! \file ostream_util.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utilities for using ostreams.
+ **
+ ** Utilities for using ostreams.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__UTIL__OSTREAM_UTIL_H
+#define __CVC4__UTIL__OSTREAM_UTIL_H
+
+#include <ios>
+#include <ostream>
+
+namespace CVC4 {
+
+// Saves the formatting of an ostream and restores the previous settings on
+// destruction. Example usage:
+//   void Foo::Print(std::ostream& out) {
+//     StreamFormatScope format_scope(out);
+//     out << std::setprecision(6) << bar();
+//   }
+class StreamFormatScope
+{
+ public:
+  // `out` must outlive StreamFormatScope.
+  StreamFormatScope(std::ostream& out);
+  ~StreamFormatScope();
+
+ private:
+  // Does not own the memory of d_out
+  std::ostream& d_out;
+  std::ios_base::fmtflags d_format_flags;
+  std::streamsize d_precision;
+};
+
+}  // namespace CVC4
+
+#endif /* __CVC4__UTIL__OSTREAM_UTIL_H */
diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp
index 61dbccbee..504d58b0e 100644
--- a/src/util/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -30,6 +30,7 @@
 
 #include "base/cvc4_assert.h"
 #include "options/set_language.h"
+#include "util/ostream_util.h"
 #include "util/smt2_quote_string.h"
 
 namespace CVC4 {
@@ -219,6 +220,8 @@ void SExpr::toStream(std::ostream& out, const SExpr& sexpr,
 
 void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr,
                         OutputLanguage language, int indent) {
+  StreamFormatScope scope(out);
+
   if (sexpr.isInteger()) {
     out << sexpr.getIntegerValue();
   } else if (sexpr.isRational()) {
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index 11afb99ed..4e2b06d53 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -19,7 +19,7 @@
 
 #include "base/cvc4_assert.h"
 #include "lib/clock_gettime.h"
-
+#include "util/ostream_util.h"
 
 #ifdef CVC4_STATISTICS_ON
 #  define __CVC4_USE_STATISTICS true
@@ -134,6 +134,7 @@ inline bool operator>=(const timespec& a, const timespec& b) {
 /** Output a timespec on an output stream. */
 std::ostream& operator<<(std::ostream& os, const timespec& t) {
   // assumes t.tv_nsec is in range
+  StreamFormatScope format_scope(os);
   return os << t.tv_sec << "."
             << std::setfill('0') << std::setw(9) << std::right << t.tv_nsec;
 }