about summary refs log tree commit diff homepage
path: root/test/Feature/LinkLLVMLib.c
diff options
context:
space:
mode:
authorMartinNowack <martin.nowack@gmail.com>2016-02-26 22:36:28 +0100
committerMartinNowack <martin.nowack@gmail.com>2016-02-26 22:36:28 +0100
commit29fc0df056dcdc7cacc1627ba80d12da6d3ef493 (patch)
treebd9c2a0a225ebdd3a475158c4004b8a51f78f030 /test/Feature/LinkLLVMLib.c
parentf76b6c5fe0ce8920ee6edb13802f857dae49e785 (diff)
parent66f53aac10962db150aec07b96f3b0a756eef28b (diff)
downloadklee-29fc0df056dcdc7cacc1627ba80d12da6d3ef493.tar.gz
Merge pull request #346 from omeranson/libraries_squashed
Added support to load libraries from command line
Diffstat (limited to 'test/Feature/LinkLLVMLib.c')
-rw-r--r--test/Feature/LinkLLVMLib.c24
1 files changed, 24 insertions, 0 deletions
diff --git a/test/Feature/LinkLLVMLib.c b/test/Feature/LinkLLVMLib.c
new file mode 100644
index 00000000..7639bfef
--- /dev/null
+++ b/test/Feature/LinkLLVMLib.c
@@ -0,0 +1,24 @@
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc -DLINK_LLVM_LIB_TEST_LIB
+// RUN: llvm-ar r %t1.a %t1.bc
+//
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t2.bc -DLINK_LLVM_LIB_TEST_EXEC
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --link-llvm-lib %t1.a --output-dir=%t.klee-out --emit-all-errors %t2.bc 2>&1 | FileCheck %s
+
+#ifdef LINK_LLVM_LIB_TEST_EXEC
+extern void printint(int d);
+
+int main(int argc, char * argv[]) {
+	printint(5);
+	// CHECK: KLEE: WARNING ONCE: calling external: printf
+	return 0;
+}
+#endif
+
+#ifdef LINK_LLVM_LIB_TEST_LIB
+#include <stdio.h>
+
+void printint(int d) {
+	printf("%d\n", d);
+}
+#endif