Admin/Windows/exec_process/exec_process.c
author wenzelm
Fri, 20 Jul 2012 16:47:17 +0200
changeset 48367 680d297ec71b
parent 48197 b13dd10ebc77
permissions -rw-r--r--
some basic Isabelle options;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
     1
/*  Author:     Makarius
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
     2
47797
63152f78e18b general exec_process -- nothing specific to Cygwin;
wenzelm
parents: 47796
diff changeset
     3
Bash process group invocation.
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
     4
*/
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
     5
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
     6
#include <stdlib.h>
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
     7
#include <stdio.h>
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
     8
#include <sys/types.h>
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
     9
#include <unistd.h>
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    10
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    11
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    12
static void fail(const char *msg)
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    13
{
47798
03ab3bd78282 print errors on stderr;
wenzelm
parents: 47797
diff changeset
    14
  fprintf(stderr, "%s\n", msg);
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    15
  exit(2);
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    16
}
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    17
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    18
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    19
int main(int argc, char *argv[])
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    20
{
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    21
  /* args */
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    22
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    23
  if (argc != 3) {
47798
03ab3bd78282 print errors on stderr;
wenzelm
parents: 47797
diff changeset
    24
    fprintf(stderr, "Bad arguments\n");
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    25
    exit(1);
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    26
  }
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    27
  char *pid_name = argv[1];
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    28
  char *script = argv[2];
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    29
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    30
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    31
  /* report pid */
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    32
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    33
  FILE *pid_file;
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    34
  pid_file = fopen(pid_name, "w");
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    35
  if (pid_file == NULL) fail("Cannot open pid file");
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    36
  fprintf(pid_file, "%d", getpid());
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    37
  fclose(pid_file);
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    38
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    39
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    40
  /* setsid */
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    41
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    42
  if (getgid() == getpid()) fail("Cannot set session id");
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    43
  setsid();
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    44
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    45
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    46
  /* exec */
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    47
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    48
  char *cmd_line[4];
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    49
  cmd_line[0] = "/bin/bash";
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    50
  cmd_line[1] = "-c";
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    51
  cmd_line[2] = script;
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    52
  cmd_line[3] = NULL;
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    53
47796
c37411691ee7 more direct exec with synchronous exit code;
wenzelm
parents: 47764
diff changeset
    54
  execv("/bin/bash", cmd_line);
c37411691ee7 more direct exec with synchronous exit code;
wenzelm
parents: 47764
diff changeset
    55
  fail("Cannot exec process");
47764
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    56
}
d141f1193789 more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash;
wenzelm
parents:
diff changeset
    57