about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--test/Feature/FunctionPointer.c26
1 files changed, 20 insertions, 6 deletions
diff --git a/test/Feature/FunctionPointer.c b/test/Feature/FunctionPointer.c
index bed9ad5e..649946dc 100644
--- a/test/Feature/FunctionPointer.c
+++ b/test/Feature/FunctionPointer.c
@@ -1,6 +1,8 @@
-// RUN: %clang %s -emit-llvm -g -c -o %t1.bc
+// RUN: %clang %s -emit-llvm -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --write-no-tests --exit-on-error %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --write-no-tests --exit-on-error %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
 
 #include <stdio.h>
 
@@ -15,23 +17,35 @@ int main(int argc, char **argv) {
   void (*fp)(const char *) = foo;
 
   printf("going to call through fp\n");
+  // CHECK: foo: called via fp
   fp("called via fp");
 
   printf("calling via pass through\n");
+  // CHECK: foo: called via bar
   bar(foo);
-        
+
   fp = baz;
+  // CHECK: baz: called via fp
   fp("called via fp");
 
+  // CHECK: foo: called via xx
   xx("called via xx");
 
-#if 0
   klee_make_symbolic(&fp, sizeof fp, "fp");
   if(fp == baz) {
+    // CHECK: baz: calling via simple symbolic!
     printf("fp = %p, baz = %p\n", fp, baz);
-    fp("calling via symbolic!");
+    fp("calling via simple symbolic!");
+    return 0;
+  }
+
+  void (*fp2)(const char *);
+  klee_make_symbolic(&fp2, sizeof fp2, "fp2");
+  if(fp2 == baz || fp2 == foo) {
+    // CHECK-DAG: baz: calling via symbolic!
+    // CHECK-DAG: foo: calling via symbolic!
+    fp2("calling via symbolic!");
   }
-#endif
 
   return 0;
 }