1 files changed, 76 insertions, 0 deletions
diff --git a/runtime/svcomp64/functions.c b/runtime/svcomp64/functions.c
new file mode 100644
index 00000000..0fdae3bd
--- /dev/null
+++ b/runtime/svcomp64/functions.c
@@ -0,0 +1,76 @@
+//===-- functions.c           ---------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/klee_svcomp.h"
+
+#define SVCOMP_NONDET_DEFN_D(NAME,T) \
+T __VERIFIER_nondet_ ## NAME() { \
+  T initialValue; \
+  klee_make_symbolic(&initialValue,\
+                     sizeof(T),\
+                     "svcomp.sym" # T);\
+  return initialValue; \
+}
+
+#define SVCOMP_NONDET_DEFN(NAME) SVCOMP_NONDET_DEFN_D(NAME, NAME)
+
+#define SVCOMP_NONDET_DEFN_NOT_SUPPORTED(NAME) \
+    SVCOMP_NONDET_DEFN_D_NOT_SUPPORTED(NAME, NAME)
+
+SVCOMP_NONDET_DEFN_D(bool,_Bool)
+SVCOMP_NONDET_DEFN(char)
+SVCOMP_NONDET_DEFN(int)
+SVCOMP_NONDET_DEFN(long)
+SVCOMP_NONDET_DEFN(loff_t)
+SVCOMP_NONDET_DEFN_D(pointer,void*)
+SVCOMP_NONDET_DEFN_D(pchar,char*)
+SVCOMP_NONDET_DEFN(pthread_t)
+SVCOMP_NONDET_DEFN(sector_t)
+SVCOMP_NONDET_DEFN(short)
+SVCOMP_NONDET_DEFN(size_t)
+SVCOMP_NONDET_DEFN_D(u32, uint32_t)
+SVCOMP_NONDET_DEFN_D(uchar,unsigned char)
+SVCOMP_NONDET_DEFN_D(uint, unsigned int)
+SVCOMP_NONDET_DEFN_D(ulong, unsigned long)
+SVCOMP_NONDET_DEFN(unsigned)
+SVCOMP_NONDET_DEFN_D(ushort, unsigned short)
+
+float __VERIFIER_nondet_float() {
+  union {
+    uint32_t asBits;
+    float asFloat;
+  } data;
+  klee_warning("Symbolic data of type float not supported. Returning quiet NaN");
+  data.asBits = 0x7fc00000;
+  return data.asFloat;
+}
+
+void __VERIFIER_assume(int condition) {
+  klee_assume(condition);
+}
+
+void __VERIFIER_assert(int cond) {
+  if (!cond) {
+    klee_report_error(__FILE__, __LINE__ ,
+                      "svcomp assert failed",
+                      "svcomp.assertfail");
+  }
+}
+
+__attribute__ ((__noreturn__)) void __VERIFIER_error()  {
+  klee_report_error(__FILE__, __LINE__,"svcomp error", "svcomp.err");
+}
+
+void __VERIFIER_atomic_begin() {
+  klee_warning("__VERIFIER_atomic_begin() is a no-op");
+}
+
+void __VERIFIER_atomic_end() {
+  klee_warning("__VERIFIER_atomic_end() is a no-op");
+}