1 files changed, 75 insertions, 0 deletions
diff --git a/test/Runtime/svcomp/verifier_nondet.c b/test/Runtime/svcomp/verifier_nondet.c
new file mode 100644
index 00000000..f95e2a52
--- /dev/null
+++ b/test/Runtime/svcomp/verifier_nondet.c
@@ -0,0 +1,75 @@
+// // Test for 32-bit
+// RUN: %llvmgcc %s -emit-llvm -m32 -g -std=c99 -c -o %t_32.bc
+// RUN: rm -rf %t.klee-out_32
+// RUN: %klee --output-dir=%t.klee-out_32 --svcomp-runtime %t_32.bc > %t.kleeoutput.32.log 2>&1
+// RUN: FileCheck -check-prefix=first-CHECK -input-file=%t.kleeoutput.32.log %s
+// RUN: FileCheck -check-prefix=second-CHECK -input-file=%t.kleeoutput.32.log %s
+// RUN: not test -f %t.klee-out_32/test*.err
+// Test again for 64-bit
+// RUN: %llvmgcc %s -emit-llvm -m64 -g -std=c99 -c -o %t_64.bc
+// RUN: rm -rf %t.klee-out_64
+// RUN: %klee --output-dir=%t.klee-out_64 --svcomp-runtime %t_64.bc > %t.kleeoutput.64.log 2>&1
+// RUN: FileCheck -check-prefix=first-CHECK -input-file=%t.kleeoutput.64.log %s
+// RUN: FileCheck -check-prefix=second-CHECK -input-file=%t.kleeoutput.64.log %s
+// RUN: not test -f %t.klee-out_64/test*.err
+
+// first-CHECK: completed paths = 1
+// second-CHECK-NOT: ERROR
+// second-CHECK-NOT: abort
+#include "klee/klee.h"
+#include "klee/klee_svcomp.h"
+
+#define test_call_D(NAME,T) \
+{ \
+  T initialValue = __VERIFIER_nondet_ ## NAME(); \
+  if (!klee_is_symbolic(initialValue)) { \
+    klee_warning("Failed to get symbolic value for type " # T); \
+    klee_abort(); \
+  } \
+}
+
+#define test_call_ptr_D(NAME,T) \
+{ \
+  T initialValue = __VERIFIER_nondet_ ## NAME(); \
+  if (!klee_is_symbolic((uintptr_t) initialValue)) { \
+    klee_warning("Failed to get symbolic value for type " # T); \
+    klee_abort(); \
+  } \
+}
+
+#define test_call(NAME) test_call_D(NAME,NAME)
+#define test_call_ptr(NAME) test_call_ptr_D(NAME,NAME)
+
+int main() {
+  test_call_D(bool,_Bool);
+  test_call(char);
+  {
+    float initialValue = __VERIFIER_nondet_float();
+    if (klee_is_symbolic(initialValue)) {
+      klee_warning("Did not expect float to be symbolic");
+      klee_abort();
+    }
+  }
+  test_call(int)
+  test_call(long)
+  test_call(loff_t)
+  test_call_ptr_D(pointer,void*)
+  test_call_ptr_D(pchar,char*)
+  {
+    pthread_t initialValue = __VERIFIER_nondet_pthread_t();
+    if (!klee_is_symbolic(initialValue.id)) {
+    klee_warning("Failed to get symbolic value for id field");
+    klee_abort();
+    }
+  }
+  test_call(sector_t)
+  test_call(short)
+  test_call(size_t)
+  test_call_D(u32, uint32_t)
+  test_call_D(uchar,unsigned char)
+  test_call_D(uint, unsigned int)
+  test_call_D(ulong, unsigned long)
+  test_call(unsigned)
+  test_call_D(ushort, unsigned short)
+  return 0;
+}