Implement all *scanf regression tests

We already had working tests for scanf and fscanf, and can easily extend
this to all variants.

Author: tautschnig

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

@@ -3,7 +3,8 @@
 
 int main()
 {
-  sscanf();
-  assert(0);
+  char dest[10];
+  int result = sscanf("hello", "%s", dest);
+  assert(result == 1);
   return 0;
 }

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

@@ -1,8 +1,10 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
-^EXIT=0$
+
+^\[main.assertion.1\] line 8 assertion result == 1: FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

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

@@ -1,9 +1,20 @@
 #include <assert.h>
+#include <stdarg.h>
 #include <stdio.h>
 
+int xscanf(const char *format, ...)
+{
+  va_list list;
+  va_start(list, format);
+  int result = vfscanf(stdin, format, list);
+  va_end(list);
+  return result;
+}
+
 int main()
 {
-  vfscanf();
-  assert(0);
+  char dest[10];
+  int result = xscanf("%s", dest);
+  assert(result == 1);
   return 0;
 }

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

@@ -1,8 +1,10 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
-^EXIT=0$
+
+^\[main.assertion.1\] line 18 assertion result == 1: FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

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

@@ -1,9 +1,20 @@
 #include <assert.h>
+#include <stdarg.h>
 #include <stdio.h>
 
+int xscanf(const char *format, ...)
+{
+  va_list list;
+  va_start(list, format);
+  int result = vscanf(format, list);
+  va_end(list);
+  return result;
+}
+
 int main()
 {
-  vscanf();
-  assert(0);
+  char dest[10];
+  int result = xscanf("%s", dest);
+  assert(result == 1);
   return 0;
 }

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

@@ -1,8 +1,10 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
-^EXIT=0$
+
+^\[main.assertion.1\] line 18 assertion result == 1: FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

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

@@ -1,9 +1,20 @@
 #include <assert.h>
+#include <stdarg.h>
 #include <stdio.h>
 
+int xscanf(const char *format, ...)
+{
+  va_list list;
+  va_start(list, format);
+  int result = vsscanf("hello", format, list);
+  va_end(list);
+  return result;
+}
+
 int main()
 {
-  vsscanf();
-  assert(0);
+  char dest[10];
+  int result = xscanf("%s", dest);
+  assert(result == 1);
   return 0;
 }

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

@@ -1,8 +1,10 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
-^EXIT=0$
+
+^\[main.assertion.1\] line 18 assertion result == 1: FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring