From eca1ff0a116a1443d7d8dd7f2efab48de7fc4ad5 Mon Sep 17 00:00:00 2001
From: Gleb Popov <6yearold@gmail.com>
Date: Sun, 6 Oct 2019 21:20:46 +0400
Subject: Do not use klee_range() in regression/2014-09-13-debug-info.c test,
 as it is incompatible with klee_prefer_cex. Fixes
 https://github.com/klee/klee/issues/1161

While there, remove dependence on `sort` utility, which might help porting KLEE
Windows eventually.
---
 test/regression/2014-09-13-debug-info.c | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'test/regression')

diff --git a/test/regression/2014-09-13-debug-info.c b/test/regression/2014-09-13-debug-info.c
index 5cad27f3..ced6d49a 100644
--- a/test/regression/2014-09-13-debug-info.c
+++ b/test/regression/2014-09-13-debug-info.c
@@ -8,13 +8,13 @@
 // one with the prefered CEX. We verify this by using ktest-tool to dump the
 // values, and then checking the output.
 //
-// RUN: /bin/sh -c "ktest-tool %t.klee-out/*.ktest" | sort > %t.data-values
+// RUN: /bin/sh -c "ktest-tool %t.klee-out/*.ktest" > %t.data-values
 // RUN: FileCheck < %t.data-values %s
 
-// CHECK: object 0: int : 0
-// CHECK: object 0: int : 17
-// CHECK: object 0: int : 32
-// CHECK: object 0: int : 99
+// CHECK-DAG: object 0: int : 0
+// CHECK-DAG: object 0: int : 17
+// CHECK-DAG: object 0: int : 32
+// CHECK-DAG: object 0: int : 99
 
 #include "klee/klee.h"
 
@@ -24,7 +24,9 @@ void f2(void) {}
 void f3(void) {}
 
 int main() {
-  int x = klee_range(0, 256, "x");
+  int x;
+  klee_make_symbolic(&x, sizeof x, "x");
+  klee_assume((unsigned) x < 256);
 
   if (x == 17) {
     f0();
-- 
cgit 1.4.1