vasprintf (char * * ret, const char * fmt, char * ap)
{
  char * ap2.0;
  int D.3757;
  int D.3759;
  char * buf;
  int len;
  size_t buflen;
  char * ap2;

  try
    {
      __builtin_va_copy (&ap2, ap);
      ap2.0 = ap2;
      len = vsnprintf (0B, 0, fmt, ap2.0);
      if (len >= 0) goto <D.3756>; else goto <D.3754>;
      <D.3756>:
      D.3757 = len + 1;
      buflen = (size_t) D.3757;
      buf = malloc (buflen);
      if (buf != 0B) goto <D.3758>; else goto <D.3754>;
      <D.3758>:
      len = vsnprintf (buf, buflen, fmt, ap);
      *ret = buf;
      goto <D.3755>;
      <D.3754>:
      *ret = 0B;
      len = -1;
      <D.3755>:
      __builtin_va_end (&ap2);
      D.3759 = len;
      return D.3759;
    }
  finally
    {
      ap2 = {CLOBBER};
    }
}


vsnprintf (char * restrict __s, size_t __n, const char * restrict __fmt, char * __ap)
{
  int D.3762;
  long unsigned int D.3763;

  D.3763 = __builtin_object_size (__s, 1);
  D.3762 = __builtin___vsnprintf_chk (__s, __n, 1, D.3763, __fmt, __ap);
  return D.3762;
}