Merge pull request #8237 from tautschnig/features/asprintf

C library: model asprintf, test {v,}asprintf

Author: kroening

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;
+}

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

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;
 }

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$

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)
   {