Merge pull request #7901 from tautschnig/features/usleep

C library: model usleep

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$

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

@@ -0,0 +1,14 @@
+#include <assert.h>
+#ifndef _WIN32
+#  include <unistd.h>
+#else
+int _usleep(unsigned);
+#endif
+
+int main()
+{
+  unsigned input;
+  int retval = _usleep(input);
+  assert(retval == 0 || retval == -1);
+  return 0;
+}

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

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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

@@ -0,0 +1,14 @@
+#include <assert.h>
+#ifndef _WIN32
+#  include <unistd.h>
+#else
+int usleep(unsigned);
+#endif
+
+int main()
+{
+  unsigned input;
+  int retval = usleep(input);
+  assert(retval == 0 || retval == -1);
+  return 0;
+}

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

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/library/unistd.c

@@ -22,6 +22,41 @@ unsigned int _sleep(unsigned int seconds)
   return sleep(seconds);
 }
 
+/* FUNCTION: usleep */
+
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+
+int usleep(unsigned int usec)
+{
+__CPROVER_HIDE:;
+  // do nothing, but return nondet value
+  __CPROVER_bool error = __VERIFIER_nondet___CPROVER_bool();
+  if(error)
+  {
+    if(usec >= 1000000)
+      errno = EINVAL;
+    else
+      errno = EINTR;
+    return -1;
+  }
+  return 0;
+}
+
+/* FUNCTION: _usleep */
+
+int usleep(unsigned int);
+
+int _usleep(unsigned int usec)
+{
+__CPROVER_HIDE:;
+  return usleep(usec);
+}
+
 /* FUNCTION: unlink */
 
 int __VERIFIER_nondet_int(void);