diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-02-12 11:30:59 -0800 |
---|---|---|
committer | Mathias Preiner <mathias.preiner@gmail.com> | 2019-02-12 11:30:59 -0800 |
commit | 6b07347b4964ff79dc6a17f22ab4be29aa489196 (patch) | |
tree | 91df594709f62a63131d06e9c07c66fb8392f4cd /src | |
parent | c86e0178bfaa662b6586d866c953a56f81cefe51 (diff) |
Delete temporary proof files when aborting CVC4 (#2834)
CVC4 was not deleting temporary proof files when crashing or being
terminated externally. This commit uses an early `unlink()` to remove
the files as soon as CVC4 terminates.
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine_check_proof.cpp | 26 |
1 files changed, 8 insertions, 18 deletions
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index c86ec7a89..c2054e1e5 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -43,23 +43,10 @@ using namespace CVC4; using namespace std; namespace CVC4 { - namespace proof { - extern const char *const plf_signatures; -}/* CVC4::proof namespace */ - -namespace smt { - -class UnlinkProofFile { - string d_filename; -public: - UnlinkProofFile(const char* filename) : d_filename(filename) {} - ~UnlinkProofFile() { unlink(d_filename.c_str()); } -};/* class UnlinkProofFile */ - -}/* CVC4::smt namespace */ - -}/* CVC4 namespace */ +extern const char *const plf_signatures; +} // namespace proof +} // namespace CVC4 void SmtEngine::checkProof() { @@ -108,8 +95,11 @@ void SmtEngine::checkProof() { return; } - // ensure this temp file is removed after - smt::UnlinkProofFile unlinker(pfFile); + // unlink() only deletes files after all processes have closed that file, so + // it is safe to unlink the proof file here. This ensures that the proof file + // is deleted even if CVC4 crashes or is terminated externally (e.g. because + // of a timeout). + unlink(pfFile); ofstream pfStream(pfFile); pfStream << proof::plf_signatures << endl; |