C library: provide implementations of fopen64, freopen64

Some implementations map fopen and freopen, respectively, to the above
when large-file support is enabled. To us, large-file support makes no
difference, so just use a single implementation for both cases.

Will eventually fix Debian bug report 1069438.

Author: tautschnig

src/ansi-c/library/stdio.c

@@ -72,35 +72,12 @@ __CPROVER_HIDE:;
 
 void fclose_cleanup(void *stream);
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+FILE *fopen64(const char *filename, const char *mode)
 
-FILE *fopen(const char *filename, const char *mode)
+  FILE *fopen(const char *filename, const char *mode)
 {
   __CPROVER_HIDE:;
-  (void)*filename;
-  (void)*mode;
-#ifdef __CPROVER_STRING_ABSTRACTION
-  __CPROVER_assert(__CPROVER_is_zero_string(filename), "fopen zero-termination of 1st argument");
-  __CPROVER_assert(__CPROVER_is_zero_string(mode), "fopen zero-termination of 2nd argument");
-#endif
-
-  FILE *fopen_result;
-
-  __CPROVER_bool fopen_error=__VERIFIER_nondet___CPROVER_bool();
-
-#if !defined(__linux__) || defined(__GLIBC__)
-  fopen_result=fopen_error?NULL:malloc(sizeof(FILE));
-#else
-  // libraries need to expose the definition of FILE; this is the
-  // case for musl
-  fopen_result=fopen_error?NULL:malloc(sizeof(int));
-#endif
-
-#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
-  __CPROVER_set_must(fopen_result, "open");
-  __CPROVER_cleanup(fopen_result, fclose_cleanup);
-#endif
-
-  return fopen_result;
+    return fopen64(filename, mode);
 }
 
 /* FUNCTION: _fopen */
@@ -152,14 +129,77 @@ __CPROVER_HIDE:;
 }
 #endif
 
+/* FUNCTION: fopen64 */
+
+#ifndef __CPROVER_STDIO_H_INCLUDED
+#  include <stdio.h>
+#  define __CPROVER_STDIO_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDLIB_H_INCLUDED
+#  include <stdlib.h>
+#  define __CPROVER_STDLIB_H_INCLUDED
+#endif
+
+void fclose_cleanup(void *stream);
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+
+FILE *fopen64(const char *filename, const char *mode)
+{
+__CPROVER_HIDE:;
+  (void)*filename;
+  (void)*mode;
+#ifdef __CPROVER_STRING_ABSTRACTION
+  __CPROVER_assert(
+    __CPROVER_is_zero_string(filename),
+    "fopen zero-termination of 1st argument");
+  __CPROVER_assert(
+    __CPROVER_is_zero_string(mode), "fopen zero-termination of 2nd argument");
+#endif
+
+  FILE *fopen_result;
+
+  __CPROVER_bool fopen_error = __VERIFIER_nondet___CPROVER_bool();
+
+#if !defined(__linux__) || defined(__GLIBC__)
+  fopen_result = fopen_error ? NULL : malloc(sizeof(FILE));
+#else
+  // libraries need to expose the definition of FILE; this is the
+  // case for musl
+  fopen_result = fopen_error ? NULL : malloc(sizeof(int));
+#endif
+
+#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+  __CPROVER_set_must(fopen_result, "open");
+  __CPROVER_cleanup(fopen_result, fclose_cleanup);
+#endif
+
+  return fopen_result;
+}
+
 /* FUNCTION: freopen */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED
 #include <stdio.h>
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+FILE *freopen64(const char *filename, const char *mode, FILE *f);
+
 FILE *freopen(const char *filename, const char *mode, FILE *f)
+{
+__CPROVER_HIDE:;
+  return freopen64(filename, mode, f);
+}
+
+/* FUNCTION: freopen64 */
+
+#ifndef __CPROVER_STDIO_H_INCLUDED
+#  include <stdio.h>
+#  define __CPROVER_STDIO_H_INCLUDED
+#endif
+
+FILE *freopen64(const char *filename, const char *mode, FILE *f)
 {
   __CPROVER_HIDE:;
   (void)*filename;

src/ansi-c/library_check.sh

@@ -55,6 +55,8 @@ perl -p -i -e 's/^__swbuf\n//' __functions # putc, FreeBSD
 perl -p -i -e 's/^__CPROVER_deallocate\n//' __functions # free-01
 perl -p -i -e 's/^__builtin_alloca\n//' __functions # alloca-01
 perl -p -i -e 's/^fclose_cleanup\n//' __functions # fopen
+perl -p -i -e 's/^fopen64\n//' __functions # fopen
+perl -p -i -e 's/^freopen64\n//' __functions # freopen
 perl -p -i -e 's/^munmap\n//' __functions # mmap-01
 perl -p -i -e 's/^__fgets_chk\n//' __functions # fgets-01/__fgets_chk.desc
 perl -p -i -e 's/^__fprintf_chk\n//' __functions # fprintf-01/__fprintf_chk.desc