Merge pull request #6095 from tautschnig/sleep

C library: make sleep() branch free

Author: tautschnig

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

@@ -1,9 +1,12 @@
 #include <assert.h>
-#include <unistd.h>
+#ifndef _WIN32
+#  include <unistd.h>
+#else
+unsigned sleep(unsigned);
+#endif
 
 int main()
 {
-  sleep();
-  assert(0);
+  assert(sleep(42) <= 42);
   return 0;
 }

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

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

src/ansi-c/library/unistd.c

@@ -7,8 +7,7 @@ unsigned int sleep(unsigned int seconds)
   __CPROVER_HIDE:;
   // do nothing, but return nondet value
   unsigned remaining_time=__VERIFIER_nondet_unsigned();
-
-  if(remaining_time>seconds) remaining_time=seconds;
+  __CPROVER_assume(remaining_time <= seconds);
 
   return remaining_time;
 }