1 files changed, 33 insertions, 0 deletions
diff --git a/runtime/Intrinsic/klee_range.c b/runtime/Intrinsic/klee_range.c
new file mode 100644
index 00000000..59d1a05e
--- /dev/null
+++ b/runtime/Intrinsic/klee_range.c
@@ -0,0 +1,33 @@
+//===-- klee_range.c ------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include <assert.h>
+#include <klee/klee.h>
+
+int klee_range(int start, int end, const char* name) {
+  int x;
+
+  assert(start < end);
+
+  if (start+1==end) {
+    return start;
+  } else {
+    klee_make_symbolic_name(&x, sizeof x, name); 
+
+    /* Make nicer constraint when simple... */
+    if (start==0) {
+      klee_assume((unsigned) x < (unsigned) end);
+    } else {
+      klee_assume(start <= x);
+      klee_assume(x < end);
+    }
+
+    return x;
+  }
+}