Merge pull request diffblue#4283 from tautschnig/fprintf

C library: Do not require stdin, stdout, stderr to be initialised

Author: tautschnig

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

@@ -3,7 +3,14 @@
 
 int main()
 {
-  fileno();
-  assert(0);
+  // requires initialization of stdin/stdout/stderr
+  // assert(fileno(stdin) == 0);
+  // assert(fileno(stdout) == 1);
+  // assert(fileno(stderr) == 2);
+
+  int fd;
+  FILE *some_file = fdopen(fd, "");
+  assert(fileno(some_file) >= -1);
+
   return 0;
 }

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

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

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

@@ -1,9 +1,9 @@
 #include <assert.h>
 #include <stdio.h>
 
-int main()
+int main(int argc, char *argv[])
 {
-  fprintf();
-  assert(0);
+  fprintf(stdout, "some string %s: %d\n", argv[0], 42);
+  fprintf(stderr, "some other string\n");
   return 0;
 }

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

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$