2 files changed, 67 insertions, 27 deletions
diff --git a/test/Feature/AddressOfLabels.c b/test/Feature/AddressOfLabels.c
index 84493fd8..6d807dbb 100644
--- a/test/Feature/AddressOfLabels.c
+++ b/test/Feature/AddressOfLabels.c
@@ -1,36 +1,38 @@
 // RUN: %llvmgcc -emit-llvm -g -c %s -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: not %klee --output-dir=%t.klee-out %t.bc 2> %t.log
-// RUN: FileCheck --input-file %t.log %s
+// RUN: %klee --output-dir=%t.klee-out %t.bc > %t.log
+// RUN: FileCheck --input-file=%t.log %s
 
-/* 
-   This currently tests that KLEE clearly reports that it doesn't
-   support taking the address of the labels, in particular
-   blockaddress constants.
+#include <stdio.h>
 
-   The test would need to be changes once support for this feature is
-   added. 
-*/
+int main(int argc, char * argv[]) {
+	// prevent CFGSimplificationPass optimisation
+	void * dummy = &&one;
+	switch(argc) {
+		case 1: break;
+		case 2:
+			dummy = &&three;
+			goto *dummy;
+		default:
+			goto *dummy;
+	}
 
-#include <stdio.h>
+	// the real test
+	void * lptr = &&two;
+	goto *lptr;
 
-int main (int argc, char** argv)
-{
-  int i = 1;
-  // CHECK: Cannot handle constant 'i8* blockaddress 
-  // CHECK: AddressOfLabels.c:[[@LINE+1]]
-  void * lptr = &&one;
+one:
+	puts("Label one");
+// CHECK-NOT: Label one
+	return 1;
 
-  if (argc > 1)
-    lptr = &&two;
-  
-  goto *lptr;
+two:
+	puts("Label two");
+// CHECK: Label two
+	return 0;
 
- one:
-  printf("argc is 1\n");
-  return 0;
-  
- two:
-  printf("argc is >1\n");
-  return 0;
+three:
+	puts("Label three");
+// CHECK-NOT: Label three
+	return 1;
 }
diff --git a/test/Feature/AddressOfLabelsSymbolic.c b/test/Feature/AddressOfLabelsSymbolic.c
new file mode 100644
index 00000000..2c7e39c7
--- /dev/null
+++ b/test/Feature/AddressOfLabelsSymbolic.c
@@ -0,0 +1,38 @@
+// RUN: %llvmgcc -emit-llvm -g -c %s -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out %t.bc > %t.log 2> %t.stderr.log
+// RUN: FileCheck %s -check-prefix=CHECK-MSG --input-file=%t.log
+// RUN: FileCheck %s -check-prefix=CHECK-ERR --input-file=%t.stderr.log
+
+#include <stdio.h>
+
+int main(void) {
+	void * lptr = &&one;
+	lptr = &&two;
+	lptr = &&three;
+
+	klee_make_symbolic(&lptr, sizeof(lptr), "lptr");
+// CHECK-ERR: KLEE: ERROR: {{.*}} indirectbr: illegal label address
+	goto *lptr;
+
+one:
+	puts("Label one");
+// CHECK-MSG-DAG: Label one
+	return 0;
+
+two:
+	puts("Label two");
+// CHECK-MSG-DAG: Label two
+	return 0;
+
+three:
+	puts("Label three");
+// CHECK-MSG-DAG: Label three
+	return 0;
+
+// LLVM should infer only {one, two, three} as valid targets
+four:
+	puts("Label four");
+// CHECK-MSG-NOT: Label four
+	return 0;
+}