Merge pull request #6182 from tautschnig/rand

C library: model rand, rand_r so as not to return negative numbers

Author: kroening

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

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  int r = rand();
+  assert(r >= 0);
+  return 0;
+}

regression/cbmc-library/rand-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/rand_r-01/main.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  unsigned int seed;
+  int r = rand_r(&seed);
+  assert(r >= 0);
+  return 0;
+}

regression/cbmc-library/rand_r-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/stdlib.c

@@ -564,3 +564,30 @@ long random(void)
   __CPROVER_assume(result>=0 && result<=2147483647);
   return result;
 }
+
+/* FUNCTION: rand */
+
+int __VERIFIER_nondet_int();
+
+int rand(void)
+{
+__CPROVER_HIDE:;
+  // We return a non-deterministic value instead of a random one.
+  int result = __VERIFIER_nondet_int();
+  __CPROVER_assume(result >= 0);
+  return result;
+}
+
+/* FUNCTION: rand_r */
+
+int __VERIFIER_nondet_int();
+
+int rand_r(unsigned int *seed)
+{
+__CPROVER_HIDE:;
+  // We return a non-deterministic value instead of a random one.
+  (void)*seed;
+  int result = __VERIFIER_nondet_int();
+  __CPROVER_assume(result >= 0);
+  return result;
+}