File tree Expand file tree Collapse file tree 1 file changed +7
-0
lines changed Expand file tree Collapse file tree 1 file changed +7
-0
lines changed Original file line number Diff line number Diff line change @@ -18,6 +18,7 @@ Author: Malte Mues <mail.mues@gmail.com>
1818#include < regex>
1919
2020#include " gdb_api.h"
21+
2122#include < goto-programs/goto_model.h>
2223
2324#include < util/string_utils.h>
@@ -48,25 +49,31 @@ void gdb_apit::create_gdb_process()
4849 {
4950 throw gdb_interaction_exceptiont (" could not create pipe for stdin" );
5051 }
52+
5153 if (pipe (pipe_output) == -1 )
5254 {
5355 throw gdb_interaction_exceptiont (" could not create pipe for stdout" );
5456 }
5557
5658 gdb_process = fork ();
59+
5760 if (gdb_process == -1 )
5861 {
5962 throw gdb_interaction_exceptiont (" could not create gdb process" );
6063 }
64+
6165 if (gdb_process == 0 )
6266 {
6367 // child process
6468 close (pipe_input[1 ]);
6569 close (pipe_output[0 ]);
70+
6671 dup2 (pipe_input[0 ], STDIN_FILENO);
6772 dup2 (pipe_output[1 ], STDOUT_FILENO);
6873 dup2 (pipe_output[1 ], STDERR_FILENO);
74+
6975 dprintf (pipe_output[1 ], " binary name: %s\n " , binary);
76+
7077 char *arg[] = {const_cast <char *>(" gdb" ),
7178 const_cast <char *>(" --interpreter=mi" ),
7279 const_cast <char *>(binary),
You can’t perform that action at this time.
0 commit comments