about summary refs log tree commit diff homepage
path: root/tools
diff options
context:
space:
mode:
authorCristian Cadar <cristic@cs.stanford.edu>2012-11-27 12:35:44 +0000
committerCristian Cadar <cristic@cs.stanford.edu>2012-11-27 12:35:44 +0000
commit16f7cfa06d9cd98e0451743bbe47c845ef240bfb (patch)
tree326e6dff5c0452cde3cc7f32c57f01781250cb2e /tools
parentae29e8bbcf7b8c5177daab9050fcd62cfb338115 (diff)
downloadklee-16f7cfa06d9cd98e0451743bbe47c845ef240bfb.tar.gz
Patch by Seungbeom Kim: "Interrupting KLEE's execution while a
watchdog is in effect kills the watchdog immediately, giving the user
a shell prompt prematurely while the child process is still running.
This patch keeps the watchdog running until the child is finished.
I see no need to be able to kill the watchdog forcefully, as long
as the child process can be killed forcefully with two interrupts."



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@168696 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'tools')
-rw-r--r--tools/klee/main.cpp5
1 files changed, 5 insertions, 0 deletions
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 4bbf85f8..0c485571 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -917,6 +917,10 @@ static void interrupt_handle() {
   interrupted = true;
 }
 
+static void interrupt_handle_watchdog() {
+  // just wait for the child to finish
+}
+
 // This is a temporary hack. If the running process has access to
 // externals then it can disable interrupts, which screws up the
 // normal "nice" watchdog termination process. We try to request the
@@ -1111,6 +1115,7 @@ int main(int argc, char **argv, char **envp) {
     } else if (pid) {
       fprintf(stderr, "KLEE: WATCHDOG: watching %d\n", pid);
       fflush(stderr);
+      sys::SetInterruptFunction(interrupt_handle_watchdog);
 
       double nextStep = util::getWallTime() + MaxTime*1.1;
       int level = 0;