only selectively kill child, not entire process group #2918
Conversation
1bda6cd to
6965b72
Compare
src/util/run.cpp
Outdated
| @@ -202,6 +207,8 @@ int run( | |||
| return 1; | |||
| } | |||
|
|
|||
| unregister_child(); | |||
There was a problem hiding this comment.
Asking for an unrelated fix: could the while loop above please get braces around its body? The jump in indentation looked pretty awkward at first sight.
|
|
||
| #ifdef _WIN32 | ||
| #else | ||
| std::vector<pid_t> pids_of_children; | ||
| pid_t child_pid = 0; |
There was a problem hiding this comment.
#include <vector> is probably redundant now. Actually more of the includes could be cleaned up (we don't need anything on Windows, csignal is included by the header file already).
Note that this is only part of the story: we still use |
6965b72 to
c93180a
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: c93180a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84146654
| pid_t child_pid = 0; | ||
|
|
||
| void register_child(pid_t pid) | ||
| { |
There was a problem hiding this comment.
We might want to include an invariant ensuring that only one child is registered.
If multiple child processes are actually supported here, then some kind of warning would be useful.
c93180a to
1c8fc56
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 1c8fc56).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84692107
This is a new approach to addressing the problem explained in PR #319.
It is enabled by the fact that SMT solvers are now executed with run(), as opposed to system().