diff options
author | Mark Laws <mdl@60hz.org> | 2017-08-15 01:44:54 +0900 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2017-08-14 09:44:54 -0700 |
commit | 93b2aef9e21adb05ec4a1aa2b0cf7fb39c408b51 (patch) | |
tree | 6e3c71f8f359f61e706609fb9334a7e90510301d /src/smt/smt_engine_check_proof.cpp | |
parent | 4b5460a79838e93f8d417462c930806a77c09d31 (diff) |
Build and test suite fixes for Windows (#186)
- Build fixes for Windows
- Make proof checking tempfile handling portable
- Test suite fixes for Windows
Diffstat (limited to 'src/smt/smt_engine_check_proof.cpp')
-rw-r--r-- | src/smt/smt_engine_check_proof.cpp | 33 |
1 files changed, 24 insertions, 9 deletions
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index 9a336dd4d..f25dd5a51 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -15,6 +15,12 @@ ** \todo document this file **/ +#if defined(_MSC_VER) || defined(__MINGW32__) || defined(__MINGW64__) +#include <io.h> +#endif +#include <sys/types.h> +#include <sys/stat.h> +#include <fcntl.h> #include <unistd.h> #include <cstdlib> @@ -81,16 +87,24 @@ void SmtEngine::checkProof() { return; } - char const* tempDir = getenv("TMPDIR"); - if (!tempDir) { - tempDir = "/tmp"; + char *pfFile = tempnam(NULL, "cvc4_"); + if (!pfFile) { + Notice() << "Error: couldn't get path from tempnam() during proof checking" << endl; + return; + } +#if defined(_MSC_VER) || defined(__MINGW32__) || defined(__MINGW64__) + int fd = _open(pfFile, + _O_CREAT | _O_EXCL | _O_SHORT_LIVED | _O_RDWR, + _S_IREAD | _S_IWRITE); +#else + mode_t openmode = S_IRUSR | S_IWUSR; + int fd = open(pfFile, O_CREAT | O_EXCL | O_RDWR, openmode); +#endif + if (fd == -1) { + free(pfFile); + Notice() << "Error: failed to open temporary file during proof checking" << endl; + return; } - - stringstream pfPath; - pfPath << tempDir << "/cvc4_proof.XXXXXX"; - - char* pfFile = strdup(pfPath.str().c_str()); - int fd = mkstemp(pfFile); // ensure this temp file is removed after smt::UnlinkProofFile unlinker(pfFile); @@ -109,6 +123,7 @@ void SmtEngine::checkProof() { a.compile_lib = false; init(); check_file(pfFile, a); + free(pfFile); close(fd); #else /* IS_PROOFS_BUILD */ |