only selectively kill child, not entire process group #2918
Conversation
kroening
requested review from
peterschrammel,
pkesseli and
smowton
as code owners
kroening
force-pushed
the
child_management
branch
2 times, most recently
from
1bda6cd to
6965b72
Compare
tautschnig
left a comment
tautschnig
left a comment
There was a problem hiding this comment.
So ... does it actually work as expected? One experiment is invoking CBMC from Java, then sending a TERM signal to the CBMC process -> the Java process should still terminate ok and not be killed.
| 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 |
kroening
force-pushed
the
child_management
branch
from
6965b72 to
c93180a
Compare
allredj
left a comment
allredj
left a comment
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.
There was a problem hiding this comment.
added preconditions
kroening
force-pushed
the
child_management
branch
from
c93180a to
1c8fc56
Compare
allredj
left a comment
allredj
left a comment
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().