about summary refs log tree commit diff homepage
path: root/tools/klee-replay/file-creator.c
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2019-08-09 16:01:18 +0100
committerMartinNowack <martin.nowack@gmail.com>2019-08-14 16:26:48 +0100
commit5b1214aa066b1ead91ed6df5f17eae244b932736 (patch)
tree90ed3059f506f2f2a50a2644aaf571cce7d19783 /tools/klee-replay/file-creator.c
parent88bb205e422ee2aaf75594e4e314b21f77f219e3 (diff)
downloadklee-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.c3
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,