diff options
author | MartinNowack <martin.nowack@gmail.com> | 2016-02-26 22:36:28 +0100 |
---|---|---|
committer | MartinNowack <martin.nowack@gmail.com> | 2016-02-26 22:36:28 +0100 |
commit | 29fc0df056dcdc7cacc1627ba80d12da6d3ef493 (patch) | |
tree | bd9c2a0a225ebdd3a475158c4004b8a51f78f030 /test/Feature/LinkLLVMLib.c | |
parent | f76b6c5fe0ce8920ee6edb13802f857dae49e785 (diff) | |
parent | 66f53aac10962db150aec07b96f3b0a756eef28b (diff) | |
download | klee-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.c | 24 |
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 |