More complete modelling of fgets

fgets may (and certainly does when successful) change the contents of the buffer
passed in. Building a regression test showed further deficiences in the stdio
library model: 1) MacOS uses _fdopen; 2) fclose uses free from stdlib.h.

Author: tautschnig

regression/cbmc/fgets1/main.c

@@ -0,0 +1,22 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main()
+{
+  char buffer[3]={'a', 'b', '\0'};
+  FILE *f=fdopen(0, "r");
+  if(!f)
+    return 1;
+
+  char *p=fgets(buffer, 3, f);
+  if(p)
+  {
+    assert(buffer[1]==p[1]);
+    assert(buffer[2]=='\0');
+    assert(p[1]=='b'); // expected to fail
+  }
+
+  fclose(f);
+
+  return 0;
+}

regression/cbmc/fgets1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--bounds-check --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[main.assertion.3\] assertion p\[1\]=='b': FAILURE
+\*\* 1 of 38 failed \(2 iterations\)
+--
+^warning: ignoring

src/ansi-c/library/stdio.c

@@ -65,7 +65,14 @@ inline FILE *fopen(const char *filename, const char *mode)
   FILE *fopen_result;
 
   _Bool fopen_error;
+
+  #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");
@@ -99,6 +106,11 @@ inline FILE* freopen(const char *filename, const char *mode, FILE *f)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#ifndef __CPROVER_STDLIB_H_INCLUDED
+#include <stdlib.h>
+#define __CPROVER_STDLIB_H_INCLUDED
+#endif
+
 inline int fclose(FILE *stream)
 {
   __CPROVER_HIDE:;
@@ -135,10 +147,47 @@ inline FILE *fdopen(int handle, const char *mode)
     "fdopen zero-termination of 2nd argument");
   #endif
 
+  #if !defined(__linux__) || defined(__GLIBC__)
+  FILE *f=malloc(sizeof(FILE));
+  #else
+  // libraries need to expose the definition of FILE; this is the
+  // case for musl
+  FILE *f=malloc(sizeof(int));
+  #endif
+
+  return f;
+}
+
+/* FUNCTION: _fdopen */
+
+// This is for Apple
+
+#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
+
+#ifdef __APPLE__
+inline FILE *_fdopen(int handle, const char *mode)
+{
+  __CPROVER_HIDE:;
+  (void)handle;
+  (void)*mode;
+  #ifdef __CPROVER_STRING_ABSTRACTION
+  __CPROVER_assert(__CPROVER_is_zero_string(mode),
+    "fdopen zero-termination of 2nd argument");
+  #endif
+
   FILE *f=malloc(sizeof(FILE));
 
   return f;
 }
+#endif
 
 /* FUNCTION: fgets */
 
@@ -147,7 +196,7 @@ inline FILE *fdopen(int handle, const char *mode)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-inline char *fgets(char *str, int size, FILE *stream)
+char *fgets(char *str, int size, FILE *stream)
 {
   __CPROVER_HIDE:;
   __CPROVER_bool error;
@@ -169,6 +218,16 @@ inline char *fgets(char *str, int size, FILE *stream)
     __CPROVER_is_zero_string(str)=!error;
     __CPROVER_zero_string_length(str)=resulting_size;
   }
+  #else
+  if(size>0)
+  {
+    int str_length;
+    __CPROVER_assume(str_length>=0 && str_length<size);
+    char contents_nondet[str_length];
+    __CPROVER_array_replace(str, contents_nondet);
+    if(!error)
+      str[str_length]='\0';
+  }
   #endif
 
   return error?0:str;