Merge pull request #7176 from tautschnig/feature/fscanf

C library: fscanf for modern glibc

Author: tautschnig

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

@@ -3,7 +3,11 @@
 
 int main()
 {
-  fscanf();
-  assert(0);
+  FILE *f = fopen("main.c", "r");
+  if(f == NULL)
+    return 1;
+  char dest[10];
+  int result = fscanf(f, "%s", dest);
+  assert(result == 1);
   return 0;
 }

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

@@ -1,8 +1,11 @@
 KNOWNBUG
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --string-abstraction
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+This test demonstrates a bug in string abstraction which appears to introduce a
+type inconsistency that trips up the simplifier.

src/ansi-c/library/stdio.c

@@ -844,6 +844,28 @@ __CPROVER_HIDE:;
   return result;
 }
 
+/* FUNCTION: __isoc99_fscanf */
+
+#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 __isoc99_fscanf(FILE *restrict stream, const char *restrict format, ...)
+{
+__CPROVER_HIDE:;
+  va_list list;
+  va_start(list, format);
+  int result = vfscanf(stream, format, list);
+  va_end(list);
+  return result;
+}
+
 /* FUNCTION: scanf */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED

src/goto-programs/string_instrumentation.cpp

@@ -251,7 +251,7 @@ void string_instrumentationt::do_function_call(
       do_sprintf(dest, target, lhs, arguments);
     else if(identifier=="snprintf")
       do_snprintf(dest, target, lhs, arguments);
-    else if(identifier=="fscanf")
+    else if(identifier == "fscanf" || identifier == "__isoc99_fscanf")
       do_fscanf(dest, target, lhs, arguments);
 
     remove_skip(dest);