From 4e999db5f5aab4445146773dee41c744903fa7f9 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <michael.tautschnig@qmul.ac.uk>
Date: Wed, 28 Dec 2016 10:30:20 +0000
Subject: [PATCH] C library: fflush(NULL) is permitted

fflush(NULL) flushes all open streams if the argument is NULL.
Thus `stream` must not be dereferenced unconditionally.
---
 src/ansi-c/library/stdio.c | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c
index 6b285484da3..5a9ab1e9d57 100644
--- a/src/ansi-c/library/stdio.c
+++ b/src/ansi-c/library/stdio.c
@@ -313,11 +313,12 @@ inline int fflush(FILE *stream)
   // just return nondet
   __CPROVER_HIDE:;
   int return_value;
-  (void)*stream;
+  (void)stream;
 
   #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
-  __CPROVER_assert(__CPROVER_get_must(stream, "open"),
-                   "fflush file must be open");
+  if(stream)
+    __CPROVER_assert(__CPROVER_get_must(stream, "open"),
+                     "fflush file must be open");
   #endif
 
   return return_value;