C library: implement {v,}dprintf

The model implementation has no side effects, but will make sure that
the format string pointer can be dereferenced.

Author: tautschnig

regression/cbmc-library/dprintf-01/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdio.h>
+
+int main(int argc, char *argv[])
+{
+  dprintf(1, "some string %s: %d\n", argv[0], 42);
+  dprintf(1, "some other string\n");
+  return 0;
+}

regression/cbmc-library/dprintf-01/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-library/vdprintf-01/main.c

@@ -0,0 +1,17 @@
+#include <stdarg.h>
+#include <stdio.h>
+
+int xdprintf(int fd, const char *format, ...)
+{
+  va_list list;
+  va_start(list, format);
+  int result = vdprintf(fd, format, list);
+  va_end(list);
+  return result;
+}
+
+int main()
+{
+  xdprintf(1, "%d\n", 42);
+  return 0;
+}

regression/cbmc-library/vdprintf-01/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/library/stdio.c

@@ -1540,6 +1540,55 @@ __CPROVER_HIDE:;
   return result;
 }
 
+/* FUNCTION: dprintf */
+
+#ifndef __CPROVER_STDIO_H_INCLUDED
+#  include <stdio.h>
+#  define __CPROVER_STDIO_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDARG_H_INCLUDED
+#  include <stdarg.h>
+#  define __CPROVER_STDARG_H_INCLUDED
+#endif
+
+int dprintf(int fd, const char *restrict format, ...)
+{
+__CPROVER_HIDE:;
+  va_list list;
+  va_start(list, format);
+  int result = dprintf(fd, format, list);
+  va_end(list);
+  return result;
+}
+
+/* FUNCTION: vdprintf */
+
+#ifndef __CPROVER_STDIO_H_INCLUDED
+#  include <stdio.h>
+#  define __CPROVER_STDIO_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDARG_H_INCLUDED
+#  include <stdarg.h>
+#  define __CPROVER_STDARG_H_INCLUDED
+#endif
+
+int __VERIFIER_nondet_int(void);
+
+int vdprintf(int fd, const char *restrict format, va_list arg)
+{
+__CPROVER_HIDE:;
+
+  int result = __VERIFIER_nondet_int();
+
+  (void)fd;
+  (void)*format;
+  (void)arg;
+
+  return result;
+}
+
 /* FUNCTION: vasprintf */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED