vasprintf (char * * ret, const char * fmt, char * ap)
{
  char * ap2.0;
  int D.2914;
  int D.2916;
  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.2913>; else goto <D.2911>;
      <D.2913>:
      D.2914 = len + 1;
      buflen = (size_t) D.2914;
      buf = malloc (buflen);
      if (buf != 0B) goto <D.2915>; else goto <D.2911>;
      <D.2915>:
      len = vsnprintf (buf, buflen, fmt, ap);
      *ret = buf;
      goto <D.2912>;
      <D.2911>:
      *ret = 0B;
      len = -1;
      <D.2912>:
      __builtin_va_end (&ap2);
      D.2916 = len;
      return D.2916;
    }
  finally
    {
      ap2 = {CLOBBER};
    }
}


vsnprintf (char * restrict __s, size_t __n, const char * restrict __fmt, char * __ap)
{
  int D.2919;
  unsigned int D.2920;

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