From 6a7b21b8f84035c262c2bc566a3dc35d44517d33 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Sun, 6 May 2018 09:43:26 +0100 Subject: Moved regression test to proper location. Fixes #705 --- test/Feature/StatesCoveringNew.c | 41 --------------------------------- test/regression/2014-09-13-debug-info.c | 41 +++++++++++++++++++++++++++++++++ 2 files changed, 41 insertions(+), 41 deletions(-) delete mode 100644 test/Feature/StatesCoveringNew.c create mode 100644 test/regression/2014-09-13-debug-info.c diff --git a/test/Feature/StatesCoveringNew.c b/test/Feature/StatesCoveringNew.c deleted file mode 100644 index e372e89e..00000000 --- a/test/Feature/StatesCoveringNew.c +++ /dev/null @@ -1,41 +0,0 @@ -// Check that we properly detect states covering new instructions. -// -// RUN: %llvmgcc -I../../../include %s -emit-llvm -O0 -c -o %t1.bc -// RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --only-output-states-covering-new %t1.bc - -// We expect 4 different output states, one for each named value and one "other" -// 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 --write-int %t.klee-out/*.ktest" | sort > %t.data-values -// RUN: FileCheck < %t.data-values %s - -// CHECK: object 0: data: 0 -// CHECK: object 0: data: 17 -// CHECK: object 0: data: 32 -// CHECK: object 0: data: 99 - -#include - -void f0(void) {} -void f1(void) {} -void f2(void) {} -void f3(void) {} - -int main() { - int x = klee_range(0, 256, "x"); - - if (x == 17) { - f0(); - } else if (x == 32) { - f1(); - } else if (x == 99) { - f2(); - } else { - klee_prefer_cex(&x, x == 0); - f3(); - } - - return 0; -} diff --git a/test/regression/2014-09-13-debug-info.c b/test/regression/2014-09-13-debug-info.c new file mode 100644 index 00000000..e372e89e --- /dev/null +++ b/test/regression/2014-09-13-debug-info.c @@ -0,0 +1,41 @@ +// Check that we properly detect states covering new instructions. +// +// RUN: %llvmgcc -I../../../include %s -emit-llvm -O0 -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --only-output-states-covering-new %t1.bc + +// We expect 4 different output states, one for each named value and one "other" +// 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 --write-int %t.klee-out/*.ktest" | sort > %t.data-values +// RUN: FileCheck < %t.data-values %s + +// CHECK: object 0: data: 0 +// CHECK: object 0: data: 17 +// CHECK: object 0: data: 32 +// CHECK: object 0: data: 99 + +#include + +void f0(void) {} +void f1(void) {} +void f2(void) {} +void f3(void) {} + +int main() { + int x = klee_range(0, 256, "x"); + + if (x == 17) { + f0(); + } else if (x == 32) { + f1(); + } else if (x == 99) { + f2(); + } else { + klee_prefer_cex(&x, x == 0); + f3(); + } + + return 0; +} -- cgit 1.4.1