diff options
author | Julian Büning <julian.buening@rwth-aachen.de> | 2018-07-21 23:01:54 +0200 |
---|---|---|
committer | MartinNowack <martin.nowack@gmail.com> | 2018-07-23 13:46:59 +0100 |
commit | 09bf6d322d79381de780871f26cdffc26d7dacf4 (patch) | |
tree | 1e829c75b7ee18c130698894e5583fee7300688f /test/Feature/EscapingFunctions.c | |
parent | 9358aa95f9ae94cbb4e1a9f638e953e0164da86c (diff) | |
download | klee-09bf6d322d79381de780871f26cdffc26d7dacf4.tar.gz |
ModuleUtil: improve and test valueIsOnlyCalled
* handle BlockAddress (which is not a valid function pointer) * there is no instruction with opcode 0 * add test for functionality
Diffstat (limited to 'test/Feature/EscapingFunctions.c')
-rw-r--r-- | test/Feature/EscapingFunctions.c | 49 |
1 files changed, 49 insertions, 0 deletions
diff --git a/test/Feature/EscapingFunctions.c b/test/Feature/EscapingFunctions.c new file mode 100644 index 00000000..8c9612a5 --- /dev/null +++ b/test/Feature/EscapingFunctions.c @@ -0,0 +1,49 @@ +// RUN: %llvmgcc -emit-llvm -O0 -g -c %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee -debug-print-escaping-functions --output-dir=%t.klee-out %t.bc 2> %t.log +// RUN: FileCheck --input-file=%t.log %s + +int functionpointer(void) { + return 1; +} + +int functionpointer_as_argument(void) { + return 2; +} + +short bitcasted_functionpointer(void) { + return 3; +} + +int receives_functionpointer(int (*f)(void)); + +int blockaddress(int x) { + void * target = &&one; + switch (x) { + case 1: break; + case 2: + target = &&two; + goto *target; + default: + goto *target; + } +one: + return 1; +two: + return 2; +} + +int main(int argc, char *argv[]) { + int (*f1)(void) = functionpointer; + f1(); + + receives_functionpointer(functionpointer_as_argument); + + int (*f2)(void) =(int (*)(void))bitcasted_functionpointer; + f2(); + + blockaddress(argc); + + // CHECK: KLEE: escaping functions: {{\[((functionpointer|functionpointer_as_argument|bitcasted_functionpointer), ){3}\]}} + return 0; +} |