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

  try
    {
      __builtin_va_copy (&ap2, ap);
      ap2.0 = ap2;
      len = vsnprintf (0B, 0, fmt, ap2.0);
      if (len >= 0) goto <D.2912>; else goto <D.2910>;
      <D.2912>:
      D.2913 = len + 1;
      buflen = (size_t) D.2913;
      buf = malloc (buflen);
      if (buf != 0B) goto <D.2914>; else goto <D.2910>;
      <D.2914>:
      len = vsnprintf (buf, buflen, fmt, ap);
      *ret = buf;
      goto <D.2911>;
      <D.2910>:
      *ret = 0B;
      len = -1;
      <D.2911>:
      __builtin_va_end (&ap2);
      D.2915 = len;
      return D.2915;
    }
  finally
    {
      ap2 = {CLOBBER};
    }
}


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

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