From ff0d675fc2861e34e1f0767af6b8b73e1a854889 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Mon, 28 Jun 2010 14:01:15 +0000 Subject: 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 --- tools/klee-replay/klee-replay.c | 27 +++++++++++++++++++-------- 1 file changed, 19 insertions(+), 8 deletions(-) (limited to 'tools/klee-replay') 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, -- cgit 1.4.1