CBMC library: fix dead code in pipe()

error was already guaranteed to be 1 in this branch, thus the ?: could
not actually produce both return values.

Author: tautschnig

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

@@ -6,17 +6,22 @@
 #endif
 
 #include <assert.h>
+#include <errno.h>
 
 int main()
 {
   int filedesc[2];
 
+  errno = 0;
 #ifdef _WIN32
   int ret = _pipe(filedesc, 1000, O_BINARY);
 #else
   int ret = pipe(filedesc);
 #endif
 
+  __CPROVER_assert(errno != EMFILE, "EMFILE");
+  __CPROVER_assert(errno != ENFILE, "ENFILE");
+
   __CPROVER_assume(ret == 0);
 
   char data[2] = {7, 42};

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

@@ -3,7 +3,9 @@ main.c
 
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.assertion\.4\] .* assertion data\[1\] == 31: FAILURE$
-^\*\* 1 of 5 failed
+^\[main\.assertion\.1\] line 22 EMFILE: FAILURE$
+^\[main\.assertion\.2\] line 23 ENFILE: FAILURE$
+^\[main\.assertion\.6\] .* assertion data\[1\] == 31: FAILURE$
+^\*\* 3 of 7 failed
 --
 ^warning: ignoring

src/ansi-c/library/unistd.c

@@ -59,7 +59,7 @@ int pipe(int fildes[2])
   __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
   if(error)
   {
-    errno=error==1 ? EMFILE : ENFILE;
+    errno = __VERIFIER_nondet___CPROVER_bool() ? EMFILE : ENFILE;
     return -1;
   }