diff options
author | Andres Noetzli <noetzli@stanford.edu> | 2019-07-22 18:39:12 -0400 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-07-22 15:39:12 -0700 |
commit | 5d203980cb011ce0a9aa5007d4792c1f80dd1e4b (patch) | |
tree | 2730abeaf4430217720d17aa3c5068901815291a /src/util | |
parent | ed8f4388c859595178e303f65393105e99d4eb59 (diff) |
Avoid move constructor of std::fstream for GCC < 5 (#3098)
GCC < 5 does not support the move constructor of `std::fstream` (see
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=54316 for details). This
commit wraps the `std::fstream` in an `std::unique_ptr` to work around
that issue.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/utility.cpp | 4 | ||||
-rw-r--r-- | src/util/utility.h | 9 |
2 files changed, 9 insertions, 4 deletions
diff --git a/src/util/utility.cpp b/src/util/utility.cpp index 9936504d2..97d5ef36b 100644 --- a/src/util/utility.cpp +++ b/src/util/utility.cpp @@ -25,7 +25,7 @@ namespace CVC4 { -std::fstream openTmpFile(std::string* pattern) +std::unique_ptr<std::fstream> openTmpFile(std::string* pattern) { char* tmpDir = getenv("TMPDIR"); if (tmpDir != nullptr) @@ -46,7 +46,7 @@ std::fstream openTmpFile(std::string* pattern) { CVC4_FATAL() << "Could not create temporary file " << *pattern; } - std::fstream tmpStream(tmpName); + std::unique_ptr<std::fstream> tmpStream(new std::fstream(tmpName)); close(r); *pattern = std::string(tmpName); delete[] tmpName; diff --git a/src/util/utility.h b/src/util/utility.h index a606648bd..4477fc7b2 100644 --- a/src/util/utility.h +++ b/src/util/utility.h @@ -22,6 +22,7 @@ #include <algorithm> #include <fstream> #include <functional> +#include <memory> #include <string> #include <utility> @@ -95,9 +96,13 @@ void container_to_stream(std::ostream& out, * @param pattern The filename pattern. This string is modified to contain the * name of the temporary file. * - * @return A filestream for the temporary file. + * @return A unique pointer to the filestream for the temporary file. + * + * Note: We use `std::unique_ptr<std::fstream>` instead of `std::fstream` + * because GCC < 5 does not support the move constructor of `std::fstream`. See + * https://gcc.gnu.org/bugzilla/show_bug.cgi?id=54316 for details. */ -std::fstream openTmpFile(std::string* pattern); +std::unique_ptr<std::fstream> openTmpFile(std::string* pattern); }/* CVC4 namespace */ |