Function log_open

src/log.c:73–95

@ @ requires separation: \separated(default_filename, errsv, log_handle, &errno); @ assigns log_handle; @ assigns \result,errno,*errsv; @*/

  @ assigns \result,errno,*errsv;
  @*/
int log_open(const char*default_filename, const int mode, int *errsv)
{
  log_handle=fopen(default_filename,(mode==TD_LOG_CREATE?"w":"a"));
  *errsv=errno;
#if defined(__CYGWIN__) || defined(__MINGW32__)
  if(log_handle!=NULL && mode!=TD_LOG_CREATE)
  {
    /* append doesn't work when running the executable via wine */
    if(fprintf(log_handle, "\n")<=0 || fflush(log_handle)!=0)
    {
      fclose(log_handle);
      log_handle=fopen(default_filename,"w");
      *errsv=errno;
    }
  }
#endif
  if(log_handle==NULL)
    return 0;
#if defined(HAVE_DUP2)
  dup2(fileno(log_handle),2);
#endif
  return 1;
}

/*@
  @ requires separation: \separated(default_filename, errsv, log_handle, &errno);