introduce --rng-initial-seed=<unsigned>

* move global theRNG into Executor
* pass theRNG via ctor to searchers
* remove some type warnings from RNG.cpp

Fixes #1023.

2 files changed, 52 insertions, 0 deletions

diff --git a/unittests/RNG/CMakeLists.txt b/unittests/RNG/CMakeLists.txt
new file mode 100644
index 00000000..866f9158
--- /dev/null
+++ b/unittests/RNG/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_klee_unit_test(RNGTest
+  RNGTest.cpp)
+target_link_libraries(RNGTest PRIVATE kleeSupport)
diff --git a/unittests/RNG/RNGTest.cpp b/unittests/RNG/RNGTest.cpp
new file mode 100644
index 00000000..218a15a7
--- /dev/null
+++ b/unittests/RNG/RNGTest.cpp
@@ -0,0 +1,49 @@
+#include "klee/ADT/RNG.h"
+
+#include "gtest/gtest.h"
+
+using namespace klee;
+
+/* test equality with default seed */
+TEST(RNG, InitialSeedEquality) {
+  RNG noseed;
+  RNG seed(5489U);
+
+  ASSERT_EQ(noseed.getBool(), seed.getBool());
+  ASSERT_EQ(noseed.getInt31(), seed.getInt31());
+  ASSERT_EQ(noseed.getInt32(), seed.getInt32());
+  ASSERT_EQ(noseed.getDouble(), seed.getDouble());
+  ASSERT_EQ(noseed.getDoubleL(), seed.getDoubleL());
+  ASSERT_EQ(noseed.getDoubleLR(), seed.getDoubleLR());
+  ASSERT_EQ(noseed.getFloat(), seed.getFloat());
+  ASSERT_EQ(noseed.getFloatL(), seed.getFloatL());
+  ASSERT_EQ(noseed.getFloatLR(), seed.getFloatLR());
+}
+
+
+/* test inequality with default seed */
+TEST(RNG, InitialSeedInEquality) {
+  RNG noseed;
+  RNG seed(42U);
+
+  ASSERT_NE(noseed.getInt32(), seed.getInt32());
+}
+
+
+/* test inequality with zero seed */
+TEST(RNG, InitialSeedZeroInEquality) {
+  RNG noseed;
+  RNG seed(0U);
+
+  ASSERT_NE(noseed.getInt32(), seed.getInt32());
+}
+
+
+/* test equality with seed provided by ctor and seed() */
+TEST(RNG, SeedEquality) {
+  RNG noseed;
+  noseed.seed(42U);
+  RNG seed(42U);
+
+  ASSERT_EQ(noseed.getInt32(), seed.getInt32());
+}