diff options
| author | Omer Anson <oaanson@gmail.com> | 2016-02-22 23:13:34 +0200 |
|---|---|---|
| committer | Omer Anson <oaanson@gmail.com> | 2016-02-25 20:52:39 +0200 |
| commit | 66f53aac10962db150aec07b96f3b0a756eef28b (patch) | |
| tree | bd9c2a0a225ebdd3a475158c4004b8a51f78f030 /test | |
| parent | f76b6c5fe0ce8920ee6edb13802f857dae49e785 (diff) | |
| download | klee-66f53aac10962db150aec07b96f3b0a756eef28b.tar.gz | |
Added support to load libraries from command line
This allows a user to invoke klee with specific libraries to load from
command line. This is an attempt to allow klee to run on applications
linked to external libraries.
The libraries still have to be compiled specially for klee, in a manner
similar to klee-uclibc, i.e. archives (build with llvm-ar) of llvm IR
files.
Diffstat (limited to 'test')
| -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 |