Skip to content

Commit 98325ce

Browse files
author
Daniel Kroening
committed
introduce file_rename
This avoids semantic mismatch between POSIX rename(...) and the _rename() function offered in the Win32 API. The proposed function is meant to offer the semantics of the corresponding C++17 function.
1 parent ac74e68 commit 98325ce

File tree

2 files changed

+43
-0
lines changed

2 files changed

+43
-0
lines changed

src/util/file_util.cpp

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -221,3 +221,41 @@ bool file_remove(const std::string &path)
221221
return unlink(path.c_str()) == 0;
222222
#endif
223223
}
224+
225+
void file_rename(const std::string &old_path, const std::string &new_path)
226+
{
227+
#ifdef _WIN32
228+
if(is_directory(old_path))
229+
{
230+
// rename() only renames directories, but does not move them.
231+
// MoveFile is not atomic.
232+
auto MoveFile_result =
233+
MoveFileW(widen(old_path).c_str(), widen(new_path).c_str());
234+
235+
if(MoveFile_result == 0)
236+
throw system_exceptiont("MoveFile failed");
237+
}
238+
else
239+
{
240+
// C++17 requires this to be atomic, which is delivered by
241+
// ReplaceFile(). MoveFile() or rename() do not guarantee this.
242+
// Any existing file at new_path is to be overwritten.
243+
auto ReplaceFile_result = ReplaceFileW(
244+
widen(new_path).c_str(), // note the ordering
245+
widen(old_path).c_str(),
246+
nullptr, // lpBackupFileName
247+
0, // dwReplaceFlags
248+
nullptr, // lpExclude
249+
nullptr); // lpReserved
250+
251+
if(ReplaceFile_result == 0)
252+
throw system_exceptiont("ReplaceFile failed");
253+
}
254+
#else
255+
int rename_result = rename(old_path.c_str(), new_path.c_str());
256+
257+
if(rename_result != 0)
258+
throw system_exceptiont(
259+
std::string("rename failed: ") + std::strerror(errno));
260+
#endif
261+
}

src/util/file_util.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,4 +42,9 @@ bool file_exists(const std::string &path);
4242
/// \return true if the file was deleted, false if it did not exist
4343
bool file_remove(const std::string &path);
4444

45+
/// Rename a file.
46+
/// C++17 will allow us to use std::filesystem::rename
47+
/// Throws an exception on failure.
48+
void file_rename(const std::string &old_path, const std::string &new_path);
49+
4550
#endif // CPROVER_UTIL_FILE_UTIL_H

0 commit comments

Comments
 (0)