File tree 1 file changed +7
-0
lines changed
1 file changed +7
-0
lines changed Original file line number Diff line number Diff line change 18
18
#include < regex>
19
19
20
20
#include " gdb_api.h"
21
+
21
22
#include < goto-programs/goto_model.h>
22
23
23
24
#include < util/string_utils.h>
@@ -48,25 +49,31 @@ void gdb_apit::create_gdb_process()
48
49
{
49
50
throw gdb_interaction_exceptiont (" could not create pipe for stdin" );
50
51
}
52
+
51
53
if (pipe (pipe_output) == -1 )
52
54
{
53
55
throw gdb_interaction_exceptiont (" could not create pipe for stdout" );
54
56
}
55
57
56
58
gdb_process = fork ();
59
+
57
60
if (gdb_process == -1 )
58
61
{
59
62
throw gdb_interaction_exceptiont (" could not create gdb process" );
60
63
}
64
+
61
65
if (gdb_process == 0 )
62
66
{
63
67
// child process
64
68
close (pipe_input[1 ]);
65
69
close (pipe_output[0 ]);
70
+
66
71
dup2 (pipe_input[0 ], STDIN_FILENO);
67
72
dup2 (pipe_output[1 ], STDOUT_FILENO);
68
73
dup2 (pipe_output[1 ], STDERR_FILENO);
74
+
69
75
dprintf (pipe_output[1 ], " binary name: %s\n " , binary);
76
+
70
77
char *arg[] = {const_cast <char *>(" gdb" ),
71
78
const_cast <char *>(" --interpreter=mi" ),
72
79
const_cast <char *>(binary),
You can’t perform that action at this time.
0 commit comments