diff --git a/regression/cbmc-library/asprintf-01/main.c b/regression/cbmc-library/asprintf-01/main.c
new file mode 100644
index 00000000000..7de8ccffccd
--- /dev/null
+++ b/regression/cbmc-library/asprintf-01/main.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+#include <stdio.h>
+
+int asprintf(char **ptr, const char *fmt, ...);
+
+int main()
+{
+  char *result = NULL;
+  int bytes = asprintf(&result, "%d\n", 42);
+  if(bytes != -1)
+  {
+    assert(result[bytes] == 0);
+    free(result);
+  }
+  return 0;
+}
diff --git a/regression/cbmc-library/asprintf-01/test.desc b/regression/cbmc-library/asprintf-01/test.desc
new file mode 100644
index 00000000000..980d8bba0d6
--- /dev/null
+++ b/regression/cbmc-library/asprintf-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check --unwind 10 --no-unwinding-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-library/vasprintf-01/main.c b/regression/cbmc-library/vasprintf-01/main.c
index 465173bed3a..4097696f273 100644
--- a/regression/cbmc-library/vasprintf-01/main.c
+++ b/regression/cbmc-library/vasprintf-01/main.c
@@ -1,9 +1,26 @@
 #include <assert.h>
+#include <stdarg.h>
 #include <stdio.h>
 
+int vasprintf(char **ptr, const char *fmt, va_list ap);
+
+int xasprintf(char **ptr, const char *format, ...)
+{
+  va_list list;
+  va_start(list, format);
+  int result = vasprintf(ptr, format, list);
+  va_end(list);
+  return result;
+}
+
 int main()
 {
-  vasprintf();
-  assert(0);
+  char *result = NULL;
+  int bytes = xasprintf(&result, "%d\n", 42);
+  if(bytes != -1)
+  {
+    assert(result[bytes] == 0);
+    free(result);
+  }
   return 0;
 }
diff --git a/regression/cbmc-library/vasprintf-01/test.desc b/regression/cbmc-library/vasprintf-01/test.desc
index f0af3724e85..980d8bba0d6 100644
--- a/regression/cbmc-library/vasprintf-01/test.desc
+++ b/regression/cbmc-library/vasprintf-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check --unwind 1 --unwinding-assertions
+--pointer-check --bounds-check --unwind 10 --no-unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c
index 99f1cc236da..5f2c2ce1688 100644
--- a/src/ansi-c/library/stdio.c
+++ b/src/ansi-c/library/stdio.c
@@ -1540,6 +1540,26 @@ __CPROVER_HIDE:;
   return result;
 }
 
+/* FUNCTION: asprintf */
+
+#ifndef __CPROVER_STDARG_H_INCLUDED
+#  include <stdarg.h>
+#  define __CPROVER_STDARG_H_INCLUDED
+#endif
+
+// declare here instead of relying on stdio.h as even those platforms that do
+// have it at all may require _GNU_SOURCE to be set
+int vasprintf(char **ptr, const char *fmt, va_list ap);
+
+int asprintf(char **ptr, const char *fmt, ...)
+{
+  va_list list;
+  va_start(list, fmt);
+  int result = vasprintf(ptr, fmt, list);
+  va_end(list);
+  return result;
+}
+
 /* FUNCTION: vasprintf */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED
@@ -1570,6 +1590,8 @@ int vasprintf(char **ptr, const char *fmt, va_list ap)
     return -1;
 
   *ptr=malloc(result_buffer_size);
+  if(!*ptr)
+    return -1;
   int i=0;
   for( ; i<result_buffer_size; ++i)
   {