Fixed bug reported at:

http://llvm.org/bugs/show_bug.cgi?id=7515

Bug was caused by the different behavior of klee_range during KLEE
execution vs. replay mode, for the case when start==end: during KLEE
execution, klee_range returns start, while during replay it called
klee_make_symbolic.



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@107005 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 19 insertions, 8 deletions

diff --git a/tools/klee-replay/klee-replay.c b/tools/klee-replay/klee-replay.c
index b3831968..1cbbf6d8 100644
--- a/tools/klee-replay/klee-replay.c
+++ b/tools/klee-replay/klee-replay.c
@@ -372,16 +372,27 @@ void klee_make_symbolic(void *addr, unsigned nbytes, const char *name) {
 }
 
 /* Redefined here so that we can check the value read. */
-int klee_range(int min, int max, const char* name) {
-  int r;  
-  klee_make_symbolic(&r, sizeof r, name); 
+int klee_range(int start, int end, const char* name) {
+  int r;
 
-  if (r < min || r >= max) {
-    fprintf(stderr, "klee_range(%d, %d, %s) returned invalid result: %d\n", 
-	    min, max, name, r);
+  if (start >= end) {
+    fprintf(stderr, "klee_range: invalid range\n");
     exit(1);
-  }  
-  return r;
+  }
+
+  if (start+1 == end)
+    return start;
+  else {
+    klee_make_symbolic(&r, sizeof r, name); 
+
+    if (r < start || r >= end) {
+      fprintf(stderr, "klee_range(%d, %d, %s) returned invalid result: %d\n", 
+	      start, end, name, r);
+      exit(1);
+    }
+    
+    return r;
+  }
 }
 
 void klee_report_error(const char *file, int line,