about summary refs log tree commit diff homepage
path: root/runtime
diff options
context:
space:
mode:
Diffstat (limited to 'runtime')
-rw-r--r--runtime/POSIX/fd.c6
-rw-r--r--runtime/POSIX/klee_init_env.c2
-rw-r--r--runtime/Runtest/intrinsics.c28
-rw-r--r--runtime/klee-libc/klee-choose.c4
4 files changed, 26 insertions, 14 deletions
diff --git a/runtime/POSIX/fd.c b/runtime/POSIX/fd.c
index d94604fa..b9a848d0 100644
--- a/runtime/POSIX/fd.c
+++ b/runtime/POSIX/fd.c
@@ -1251,13 +1251,13 @@ char *getcwd(char *buf, size_t size) {
 
 static void *__concretize_ptr(const void *p) {
   /* XXX 32-bit assumption */
-  char *pc = (char*) klee_get_value((unsigned) (long) p);
+  char *pc = (char*) klee_get_valuel((long) p);
   klee_assume(pc == p);
   return pc;
 }
 
 static size_t __concretize_size(size_t s) {
-  size_t sc = klee_get_value(s);
+  size_t sc = klee_get_valuel((long)s);
   klee_assume(sc == s);
   return sc;
 }
@@ -1276,7 +1276,7 @@ static const char *__concretize_string(const char *s) {
         *sc++ = '/';
       } 
     } else {
-      char cc = (char) klee_get_value(c);
+      char cc = (char) klee_get_valuel((long)c);
       klee_assume(cc == c);
       *sc++ = cc;
       if (!cc) break;
diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c
index 5c1cc4fb..2a6b6f68 100644
--- a/runtime/POSIX/klee_init_env.c
+++ b/runtime/POSIX/klee_init_env.c
@@ -8,7 +8,9 @@
 //===----------------------------------------------------------------------===//
 
 #include "klee/klee.h"
+#ifndef _LARGEFILE64_SOURCE
 #define _LARGEFILE64_SOURCE
+#endif
 #include "fd.h"
 
 #include <stdlib.h>
diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c
index 7ec21901..2302e278 100644
--- a/runtime/Runtest/intrinsics.c
+++ b/runtime/Runtest/intrinsics.c
@@ -31,7 +31,7 @@ static unsigned char rand_byte(void) {
   return x & 0xFF;
 }
 
-void klee_make_symbolic(void *array, unsigned nbytes, const char *name) {
+void klee_make_symbolic(void *array, size_t nbytes, const char *name) {
   static int rand_init = -1;
 
   if (rand_init == -1) {
@@ -52,7 +52,7 @@ void klee_make_symbolic(void *array, unsigned nbytes, const char *name) {
       *v = rand() % 69;
     } else {
       char *c = array;
-      unsigned i;
+      size_t i;
       for (i=0; i<nbytes; i++)
         c[i] = rand_byte();
     }
@@ -98,24 +98,34 @@ void klee_silent_exit(int x) {
   exit(x);
 }
 
-unsigned klee_choose(unsigned n) {
-  unsigned x;
+uintptr_t klee_choose(uintptr_t n) {
+  uintptr_t x;
   klee_make_symbolic(&x, sizeof x, "klee_choose");
   if(x >= n)
-    fprintf(stderr, "ERROR: max = %d, got = %d\n", n, x);
+    fprintf(stderr, "ERROR: max = %ld, got = %ld\n", n, x);
   assert(x < n);
   return x;
 }
 
-void klee_assume(unsigned x) {
+void klee_assume(uintptr_t x) {
   if (!x) {
     fprintf(stderr, "ERROR: invalid klee_assume\n");
   }
 }
 
-unsigned klee_get_value(unsigned x) {
-  return x;
-}
+#define KLEE_GET_VALUE_STUB(suffix, type)	\
+	type klee_get_value##suffix(type x) { \
+		return x; \
+	}
+
+KLEE_GET_VALUE_STUB(f, float)
+KLEE_GET_VALUE_STUB(d, double)
+KLEE_GET_VALUE_STUB(l, long)
+KLEE_GET_VALUE_STUB(ll, long long)
+KLEE_GET_VALUE_STUB(_i32, int32_t)
+KLEE_GET_VALUE_STUB(_i64, int64_t)
+
+#undef KLEE_GET_VALUE_STUB
 
 int klee_range(int begin, int end, const char* name) {
   int x;
diff --git a/runtime/klee-libc/klee-choose.c b/runtime/klee-libc/klee-choose.c
index 347933df..181aedaa 100644
--- a/runtime/klee-libc/klee-choose.c
+++ b/runtime/klee-libc/klee-choose.c
@@ -9,8 +9,8 @@
 
 #include "klee/klee.h"
 
-unsigned klee_choose(unsigned n) {
-  unsigned x;
+uintptr_t klee_choose(uintptr_t n) {
+  uintptr_t x;
   klee_make_symbolic(&x, sizeof x, "klee_choose");
 
   // NB: this will *not* work if they don't compare to n values.