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 | |
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')
-rw-r--r-- | test/Feature/EscapingFunctions.c | 49 | ||||
-rw-r--r-- | test/Feature/EscapingFunctionsAlias.c | 43 |
2 files changed, 92 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; +} diff --git a/test/Feature/EscapingFunctionsAlias.c b/test/Feature/EscapingFunctionsAlias.c new file mode 100644 index 00000000..7eb2a962 --- /dev/null +++ b/test/Feature/EscapingFunctionsAlias.c @@ -0,0 +1,43 @@ +// Darwin does not support strong aliases. +// REQUIRES: not-darwin +// 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 + +void global_alias(void) __attribute__((alias("global_aliasee"))); +void global_aliasee(void) { + return; +} + +short bitcast_of_alias(void) __attribute__((alias("bitcast_of_global_alias"))); +short bitcast_of_global_alias(void) { + return 1; +} + +short bitcast_of_aliasee(void) __attribute__((alias("bitcast_of_global_aliasee"))); +short bitcast_of_global_aliasee(void) { + return 1; +} + +int bitcast_in_global_alias(void) __attribute__((alias("bitcast_in_alias"))); +short bitcast_in_alias(void) { + return 1; +} + +int main(int argc, char *argv[]) { + global_aliasee(); + global_alias(); + + int (*f1)(void) =(int (*)(void))bitcast_of_alias; + f1(); + + int (*f2)(void) =(int (*)(void))bitcast_of_global_aliasee; + f2(); + + bitcast_in_alias(); + bitcast_in_global_alias(); + + // CHECK: KLEE: escaping functions: {{\[((bitcast_of_global_alias|bitcast_of_global_aliasee), ){2}\]}} + return 0; +} |