void spass_call(int argc, char ** argv, Formula * fl, ui time)
{
    int fch1[2], fch2[2];
    char ** sp_argv; ui cpid;

    sp_argv = malloc((argc + 2)*sizeof(char*));
    memcpy(sp_argv, argv, argc*sizeof(char*));
    sp_argv[argc] = "-Stdin"; sp_argv[argc + 1] = NULL;

    if (pipe(fch1) == -1) { perror("spass_call"); return; }
    if (pipe(fch2) == -1) { perror("spass_call"); return; }

    if (!(cpid = fork()))
    {
        dup2(fch1[0], 0); close(fch1[1]);
        dup2(fch2[1], 1); close(fch2[0]);
        execvp(sp_argv[0],sp_argv);
        perror("spass_call"); return;
    }
    if (cpid == -1) { perror("spass_call"); return; }

    in  = fdopen(fch2[0], "r"); close(fch2[1]);
    out = fdopen(fch1[1], "w"); close(fch1[0]);

    spass_in(fl, time); spass_out();
}

======================= Translated ===================================

void spass_call(int argc, char ** argv, Formula * fl_, ui time_)
{
    char *sp_argv  = NULL; 
    long  args_len = 0;
    int   i = 0;

    for (i=0;i<argc;i++) args_len+=strlen(argv[i])+1;
    sp_argv = (char *)malloc(args_len*sizeof(char) +
        strlen("-Stdin -DocProof=0 -PProblem=0 -PGiven=0 -CNFOptSkolem=0") + 1);
    sp_argv[0] = 0;
    for (i=0;i<argc;i++) {strcat(sp_argv,argv[i]);strcat(sp_argv," ");}
    strcat(sp_argv,"-Stdin -DocProof=0 -PProblem=0 -PGiven=0 -CNFOptSkolem=0");
    printf("Command line is:%s",sp_argv);            

    fl   = fl_;
    time = time_;
    
    run_FW_FR(sp_argv,
              SpsWriterThreadFunc,
              SpsReaderThreadFunc);    
}

DWORD WINAPI SpsReaderThreadFunc( LPVOID lpParam )
{
    DWORD bw,br;
    int c;
    IO_ ioReader = *((IO_*)lpParam);
    int res = 0;
    int prv = 0, unp = 0, bnd = 0, tim = 0;
    char * prvs = "\nSPASS beiseite: Proof found.";
    char * unps = "\nSPASS beiseite: Completion found.";
    char * bnds = "\nSPASS beiseite: Maximal number of loops exceeded.";
    char * tims = "\nSPASS beiseite: Ran out of time.";

    WriteFile(ioReader.Write,"parsing prover output",21,&bw,0);
    do
    {
     ReadFile(ioReader.Read,&c,1,&br,0);
     if (!br) break;
     WriteFile(ioReader.Write,&c,1,&bw,0);

     if (res) continue;
     if ((char)c == prvs[prv]) { if (!prvs[++prv]) res = '+'; } else prv = 0;
     if ((char)c == unps[unp]) { if (!unps[++unp]) res = '!'; } else unp = 0;
     if ((char)c == bnds[bnd]) { if (!bnds[++bnd]) res = '_'; } else bnd = 0;
     if ((char)c == tims[tim]) { if (!tims[++tim]) res = '-'; } else tim = 0;

    } while (bw);
 
    printf("\n/\n%c\n", res);

    CloseHandle(ioReader.Read);
    return 0;
}

DWORD WINAPI SpsWriterThreadFunc( LPVOID lpParam )
{
    DWORD bw,br;
    int c;
    IO_ ioWriter = *((IO_*)lpParam);

    spass_in(ioWriter.Write);
 
    CloseHandle(ioWriter.Write);
    return 0;
}

=========================== Spawn and Redirect ==========================

static
BOOL
mkAnonPipe( HANDLE* pHandleIn,  BOOL isInheritableIn,
	    HANDLE* pHandleOut, BOOL isInheritableOut
	  )
{
  HANDLE hTemporaryIn  = NULL;
  HANDLE hTemporaryOut = NULL;
  BOOL status;
  SECURITY_ATTRIBUTES sec_attrs;

  sec_attrs.nLength = sizeof(SECURITY_ATTRIBUTES); 
  sec_attrs.lpSecurityDescriptor = NULL; 
  sec_attrs.bInheritHandle = TRUE;

  status = 
    CreatePipe( ((!isInheritableIn)  ? &hTemporaryIn  : pHandleIn),
		((!isInheritableOut) ? &hTemporaryOut : pHandleOut),
		&sec_attrs,
		0);

  if ( !status ) {
    return FALSE;
  }
  
  if (!isInheritableIn) {
    status = DuplicateHandle( GetCurrentProcess(), hTemporaryIn,
			      GetCurrentProcess(), pHandleIn,
			      0,
			      FALSE, 
			      DUPLICATE_SAME_ACCESS);

    if ( !status ) {
      return FALSE;
    }
    CloseHandle(hTemporaryIn);
  }

  if (!isInheritableOut) {
    status = DuplicateHandle( GetCurrentProcess(), hTemporaryOut,
			      GetCurrentProcess(), pHandleOut,
			      0,
			      FALSE, 
			      DUPLICATE_SAME_ACCESS);

    if ( !status ) {
      return FALSE;
    }
    CloseHandle(hTemporaryOut);
  }
  
  return TRUE;
}

int
spawnProc ( char* cmd
	  , int* pFdInWrite
	  , int* pFdOutRead
	  , int* pFdErrRead
          )
{
  BOOL status;
  STARTUPINFO si;
  PROCESS_INFORMATION pi;
  HANDLE hStdinReadEnd,  hStdinWriteEnd;
  HANDLE hStdoutReadEnd, hStdoutWriteEnd;
  HANDLE hStderrReadEnd, hStderrWriteEnd;

  if ( !mkAnonPipe( &hStdinReadEnd, TRUE,
		    &hStdinWriteEnd, FALSE) ) {
    return -1;
  }
  
  if ( !mkAnonPipe( &hStdoutReadEnd, FALSE,
		    &hStdoutWriteEnd, TRUE) ) {
    CloseHandle(hStdinReadEnd);
    CloseHandle(hStdinWriteEnd);
    return -1;
  }

  if ( !mkAnonPipe( &hStderrReadEnd, FALSE,
		    &hStderrWriteEnd, TRUE) ) {
    CloseHandle(hStdinReadEnd);
    CloseHandle(hStdinWriteEnd);
    CloseHandle(hStdoutReadEnd);
    CloseHandle(hStdoutWriteEnd);
    return -1;
  }
  
  ZeroMemory(&si, sizeof(si));
  si.cb = sizeof(si);
  si.hStdInput  = hStdinReadEnd;
  si.hStdOutput = hStdoutWriteEnd;
  si.hStdError  = hStderrWriteEnd;
  si.dwFlags    = STARTF_USESTDHANDLES | STARTF_USESHOWWINDOW;
  si.wShowWindow = SW_HIDE;

  status = CreateProcess ( NULL,
			   cmd,
			   NULL,
			   NULL,
			   TRUE,
			   NORMAL_PRIORITY_CLASS,
			   NULL,
			   NULL,
			   &si,
			   &pi);
			   

  CloseHandle(hStdinReadEnd);
  CloseHandle(hStdoutWriteEnd);
  CloseHandle(hStderrWriteEnd);

  if (!status) {
    CloseHandle(hStdinWriteEnd);
    CloseHandle(hStdoutReadEnd);
    CloseHandle(hStderrReadEnd);
    return -1;
  }
  
  CloseHandle(pi.hProcess);
  CloseHandle(pi.hThread);
  
  *pFdInWrite = (int)_open_osfhandle((long)hStdinWriteEnd, _O_TEXT);
  *pFdOutRead = (int)_open_osfhandle((long)hStdoutReadEnd, _O_TEXT);
  *pFdErrRead = (int)_open_osfhandle((long)hStderrReadEnd, _O_TEXT);

  return 0;
}