From 6b07347b4964ff79dc6a17f22ab4be29aa489196 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 12 Feb 2019 11:30:59 -0800 Subject: [PATCH] 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. --- src/smt/smt_engine_check_proof.cpp | 26 ++++++++------------------ 1 file 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; -- 2.30.2