From 6a7b21b8f84035c262c2bc566a3dc35d44517d33 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <c.cadar@imperial.ac.uk>
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

(limited to 'test')

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 <klee/klee.h>
-
-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 <klee/klee.h>
+
+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