diff options
| author | Gleb Popov <6yearold@gmail.com> | 2019-10-06 21:20:46 +0400 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-10-07 13:20:18 +0100 |
| commit | eca1ff0a116a1443d7d8dd7f2efab48de7fc4ad5 (patch) | |
| tree | e4d34b202f43e2312229b09122278750b7c0b26e | |
| parent | 0aed7731210d0eb41c0ea767edb8067130cf6252 (diff) | |
| download | klee-eca1ff0a116a1443d7d8dd7f2efab48de7fc4ad5.tar.gz | |
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.
| -rw-r--r-- | test/regression/2014-09-13-debug-info.c | 14 |
1 files changed, 8 insertions, 6 deletions
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(); |