C library: Constrain the return value of fileno and test it

The earlier commit made sure it returns 0/1/2 for stdin/stdout/stderr.

Author: tautschnig

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

@@ -3,7 +3,13 @@
 
 int main()
 {
-  fileno();
-  assert(0);
+  // requires initialization of stdin/stdout/stderr
+  // assert(fileno(stdin) == 0);
+  // assert(fileno(stdout) == 1);
+  // assert(fileno(stderr) == 2);
+
+  FILE *some_file;
+  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$

src/ansi-c/library/stdio.c

@@ -391,7 +391,6 @@ int __VERIFIER_nondet_int();
 
 inline int fileno(FILE *stream)
 {
-// just return nondet
 __CPROVER_HIDE:;
   if(stream == stdin)
     return 0;
@@ -401,6 +400,7 @@ __CPROVER_HIDE:;
     return 2;
 
   int return_value=__VERIFIER_nondet_int();
+  __CPROVER_assume(return_value >= -1);
 
 #if !defined(__linux__) || defined(__GLIBC__)
   (void)*stream;