Skip to content

Commit 0d93d11

Browse files
author
Daniel Kroening
authored
Merge pull request #5238 from diffblue/file_rename
File rename
2 parents 8a24f79 + bac67a5 commit 0d93d11

File tree

5 files changed

+69
-16
lines changed

5 files changed

+69
-16
lines changed

src/goto-cc/as_mode.cpp

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ Author: Michael Tautschnig
2424
#include <cstring>
2525

2626
#include <util/config.h>
27+
#include <util/file_util.h>
2728
#include <util/get_base_name.h>
2829
#include <util/run.h>
2930
#include <util/tempdir.h>
@@ -289,14 +290,17 @@ int as_modet::as_hybrid_binary(const compilet &compiler)
289290

290291
// save the goto-cc output file
291292
std::string saved = output_file + ".goto-cc-saved";
292-
int result = rename(output_file.c_str(), saved.c_str());
293-
if(result!=0)
293+
try
294294
{
295-
error() << "Rename failed: " << std::strerror(errno) << eom;
296-
return result;
295+
file_rename(output_file, saved);
296+
}
297+
catch(const cprover_exception_baset &e)
298+
{
299+
error() << "Rename failed: " << e.what() << eom;
300+
return 1;
297301
}
298302

299-
result=run_as();
303+
int result = run_as();
300304

301305
if(result == 0)
302306
{

src/goto-cc/gcc_mode.cpp

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -937,12 +937,17 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler)
937937
it++)
938938
{
939939
std::string bin_name=*it+goto_binary_tmp_suffix;
940-
int result=rename(it->c_str(), bin_name.c_str());
941-
if(result!=0)
940+
941+
try
942942
{
943-
error() << "Rename failed: " << std::strerror(errno) << eom;
944-
return result;
943+
file_rename(*it, bin_name);
945944
}
945+
catch(const cprover_exception_baset &e)
946+
{
947+
error() << "Rename failed: " << e.what() << eom;
948+
return 1;
949+
}
950+
946951
goto_binaries.push_back(bin_name);
947952
}
948953

src/goto-cc/ld_mode.cpp

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -189,16 +189,17 @@ int ld_modet::ld_hybrid_binary(compilet &compiler)
189189
// save the goto-cc output file
190190
std::string goto_binary = output_file + goto_binary_tmp_suffix;
191191

192-
int result;
193-
194-
result = rename(output_file.c_str(), goto_binary.c_str());
195-
if(result != 0)
192+
try
193+
{
194+
file_rename(output_file, goto_binary);
195+
}
196+
catch(const cprover_exception_baset &e)
196197
{
197-
error() << "Rename failed: " << std::strerror(errno) << eom;
198-
return result;
198+
error() << "Rename failed: " << e.what() << eom;
199+
return 1;
199200
}
200201

201-
result = run_ld();
202+
int result = run_ld();
202203

203204
if(result == 0 && cmdline.isset('T'))
204205
{

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)