C library: implement {v,}snprintf

The model will non-deterministically alter the target string up to the
bound given as argument to {v,}snprintf.

Author: tautschnig

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

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdio.h>
+
+int main()
+{
+  char result[10];
+  int bytes = snprintf(result, 10, "%d\n", 42);
+  assert(bytes <= 10);
+  return 0;
+}

regression/cbmc-library/snprintf-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/vsnprintf-01/main.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+#include <stdarg.h>
+#include <stdio.h>
+
+int xsnprintf(char *ptr, size_t size, const char *format, ...)
+{
+  va_list list;
+  va_start(list, format);
+  int result = vsnprintf(ptr, size, format, list);
+  va_end(list);
+  return result;
+}
+
+int main()
+{
+  char result[10];
+  int bytes = xsnprintf(result, 10, "%d\n", 42);
+  assert(bytes <= 10);
+  return 0;
+}

regression/cbmc-library/vsnprintf-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

src/ansi-c/library/stdio.c

@@ -1584,6 +1584,72 @@ int vasprintf(char **ptr, const char *fmt, va_list ap)
   return i;
 }
 
+/* FUNCTION: snprintf */
+
+#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 snprintf(char *str, size_t size, const char *fmt, ...)
+{
+  va_list list;
+  va_start(list, fmt);
+  int result = vsnprintf(str, size, fmt, list);
+  va_end(list);
+  return result;
+}
+
+/* FUNCTION: vsnprintf */
+
+#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
+
+#ifndef __CPROVER_STDLIB_H_INCLUDED
+#  include <stdlib.h>
+#  define __CPROVER_STDLIB_H_INCLUDED
+#endif
+
+char __VERIFIER_nondet_char(void);
+
+int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
+{
+  (void)*fmt;
+
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
+        __CPROVER_OBJECT_SIZE(ap))
+
+  {
+    (void)va_arg(ap, int);
+    __CPROVER_precondition(
+      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
+      "vsnprintf object overlap");
+  }
+
+  size_t i = 0;
+  for(; i < size; ++i)
+  {
+    char c = __VERIFIER_nondet_char();
+    str[i] = c;
+    if(c == '\0')
+      break;
+  }
+
+  return i;
+}
+
 /* FUNCTION: __acrt_iob_func */
 
 #ifdef _WIN32