diff options
author | Cristian Cadar <cristic@cs.stanford.edu> | 2012-11-27 12:35:44 +0000 |
---|---|---|
committer | Cristian Cadar <cristic@cs.stanford.edu> | 2012-11-27 12:35:44 +0000 |
commit | 97f7b167ba8f8e39c4b4a42ed45dcce6ecee43b9 (patch) | |
tree | afab9203a606fc8b92303f4d177c67a2cccd64ce /klee/tools | |
parent | 712f06395eebd6183b2b49f793a7c7c5061880fa (diff) |
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."
Diffstat (limited to 'klee/tools')
-rw-r--r-- | klee/tools/klee/main.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/klee/tools/klee/main.cpp b/klee/tools/klee/main.cpp index 4bbf85f8de5..0c48557193f 100644 --- a/klee/tools/klee/main.cpp +++ b/klee/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; |