C library/scanf: havoc all target objects

scanf may write to any of the objects behind the pointer-typed
arguments.

Author: tautschnig

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

@@ -3,7 +3,20 @@
 
 int main()
 {
-  scanf();
-  assert(0);
+  scanf(""); // parse nothing, must not result in any out-of-bounds access
+  int x = 0;
+  scanf("%d", &x);
+  _Bool nondet;
+  if(nondet)
+    __CPROVER_assert(x == 0, "need not remain zero");
+  else
+    __CPROVER_assert(x != 0, "may remain zero");
+  long int lx = 0;
+  long long int llx = 0;
+  scanf("%d, %ld, %lld", &x, &lx, &llx);
+  if(nondet)
+    __CPROVER_assert(lx + llx == 0, "need not remain zero");
+  else
+    __CPROVER_assert(lx + llx != 0, "may remain zero");
   return 0;
 }

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

@@ -1,8 +1,13 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
-^EXIT=0$
+\[main.assertion.1\] line 11 need not remain zero: FAILURE$
+\[main.assertion.2\] line 13 may remain zero: FAILURE$
+\[main.assertion.3\] line 18 need not remain zero: FAILURE$
+\[main.assertion.4\] line 20 may remain zero: FAILURE$
+^\*\* 4 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

src/ansi-c/library/stdio.c

@@ -983,7 +983,12 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
   }
 
   (void)*format;
-  (void)arg;
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
+        __CPROVER_OBJECT_SIZE(arg))
+  {
+    void *a = va_arg(arg, void *);
+    __CPROVER_havoc_object(a);
+  }
 
 #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
@@ -1025,7 +1030,12 @@ __CPROVER_HIDE:;
   }
 
   (void)*format;
-  (void)arg;
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
+        __CPROVER_OBJECT_SIZE(arg))
+  {
+    void *a = va_arg(arg, void *);
+    __CPROVER_havoc_object(a);
+  }
 
 #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(
@@ -1069,7 +1079,12 @@ int __stdio_common_vfscanf(
   }
 
   (void)*format;
-  (void)args;
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) <
+        __CPROVER_OBJECT_SIZE(args))
+  {
+    void *a = va_arg(args, void *);
+    __CPROVER_havoc_object(a);
+  }
 
 #  ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(
@@ -1137,7 +1152,13 @@ int vsscanf(const char *restrict s, const char *restrict format, va_list arg)
   int result=__VERIFIER_nondet_int();
   (void)*s;
   (void)*format;
-  (void)arg;
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
+        __CPROVER_OBJECT_SIZE(arg))
+  {
+    void *a = va_arg(arg, void *);
+    __CPROVER_havoc_object(a);
+  }
+
   return result;
 }
 
@@ -1164,7 +1185,13 @@ __CPROVER_HIDE:;
   int result = __VERIFIER_nondet_int();
   (void)*s;
   (void)*format;
-  (void)arg;
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
+        __CPROVER_OBJECT_SIZE(arg))
+  {
+    void *a = va_arg(arg, void *);
+    __CPROVER_havoc_object(a);
+  }
+
   return result;
 }
 
@@ -1199,7 +1226,12 @@ int __stdio_common_vsscanf(
 
   (void)*s;
   (void)*format;
-  (void)args;
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) <
+        __CPROVER_OBJECT_SIZE(args))
+  {
+    void *a = va_arg(args, void *);
+    __CPROVER_havoc_object(a);
+  }
 
   return result;
 }