diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-08-09 16:01:18 +0100 |
---|---|---|
committer | MartinNowack <martin.nowack@gmail.com> | 2019-08-14 16:26:48 +0100 |
commit | 5b1214aa066b1ead91ed6df5f17eae244b932736 (patch) | |
tree | 90ed3059f506f2f2a50a2644aaf571cce7d19783 /tools/klee-replay/file-creator.c | |
parent | 88bb205e422ee2aaf75594e4e314b21f77f219e3 (diff) | |
download | klee-5b1214aa066b1ead91ed6df5f17eae244b932736.tar.gz |
Added an option to klee-replay to keep replay directory
Diffstat (limited to 'tools/klee-replay/file-creator.c')
-rw-r--r-- | tools/klee-replay/file-creator.c | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tools/klee-replay/file-creator.c b/tools/klee-replay/file-creator.c index 6440b414..f6a077c2 100644 --- a/tools/klee-replay/file-creator.c +++ b/tools/klee-replay/file-creator.c @@ -478,6 +478,9 @@ int remove_callback(const char *fpath, } void replay_delete_files() { + if (keep_temps) + return; + fprintf(stderr, "KLEE-REPLAY: NOTE: removing %s\n", replay_dir); if (nftw(replay_dir, remove_callback, FOPEN_MAX, |