diff options
author | Julian Büning <julian.buening@rwth-aachen.de> | 2018-07-28 10:16:26 +0200 |
---|---|---|
committer | MartinNowack <martin.nowack@gmail.com> | 2018-07-28 12:27:03 +0100 |
commit | bf85ec188e0a952b6373f378826b0e26ae60f2f8 (patch) | |
tree | 1f740067cc75634beeb2317ada9e430565559002 | |
parent | b585a94ad0cb30570cf4f14e2dc1ebb43f694bb3 (diff) | |
download | klee-bf85ec188e0a952b6373f378826b0e26ae60f2f8.tar.gz |
test/Feature/EscapingFunctionsAlias.c: clarify alias(ee) casting
-rw-r--r-- | test/Feature/EscapingFunctionsAlias.c | 22 |
1 files changed, 14 insertions, 8 deletions
diff --git a/test/Feature/EscapingFunctionsAlias.c b/test/Feature/EscapingFunctionsAlias.c index 7eb2a962..933a23ca 100644 --- a/test/Feature/EscapingFunctionsAlias.c +++ b/test/Feature/EscapingFunctionsAlias.c @@ -5,23 +5,25 @@ // RUN: %klee -debug-print-escaping-functions --output-dir=%t.klee-out %t.bc 2> %t.log // RUN: FileCheck --input-file=%t.log %s +#include <stdint.h> + 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) { +uint8_t bitcast_of_alias(void) __attribute__((alias("bitcast_of_global_alias"))); +uint8_t bitcast_of_global_alias(void) { return 1; } -short bitcast_of_aliasee(void) __attribute__((alias("bitcast_of_global_aliasee"))); -short bitcast_of_global_aliasee(void) { +uint8_t bitcast_of_aliasee(void) __attribute__((alias("bitcast_of_global_aliasee"))); +uint8_t bitcast_of_global_aliasee(void) { return 1; } -int bitcast_in_global_alias(void) __attribute__((alias("bitcast_in_alias"))); -short bitcast_in_alias(void) { +uint64_t bitcast_in_global_alias(void) __attribute__((alias("bitcast_in_alias"))); +uint8_t bitcast_in_alias(void) { return 1; } @@ -29,13 +31,17 @@ int main(int argc, char *argv[]) { global_aliasee(); global_alias(); - int (*f1)(void) =(int (*)(void))bitcast_of_alias; + // casting alias + // should result in aliasee being marked as escaping + uint64_t (*f1)(void) =(uint64_t (*)(void))bitcast_of_alias; f1(); - int (*f2)(void) =(int (*)(void))bitcast_of_global_aliasee; + // casting aliasee + uint64_t (*f2)(void) =(uint64_t (*)(void))bitcast_of_global_aliasee; f2(); bitcast_in_alias(); + // cast when aliasing should not result in either function being marked as escaping bitcast_in_global_alias(); // CHECK: KLEE: escaping functions: {{\[((bitcast_of_global_alias|bitcast_of_global_aliasee), ){2}\]}} |