diff options
author | Julian Büning <julian.buening@rwth-aachen.de> | 2018-07-24 22:04:02 +0200 |
---|---|---|
committer | MartinNowack <martin.nowack@gmail.com> | 2018-07-28 12:27:03 +0100 |
commit | b585a94ad0cb30570cf4f14e2dc1ebb43f694bb3 (patch) | |
tree | f0d0f441a86bd6685ed5add5c771ed38445b638b /test | |
parent | 09bf6d322d79381de780871f26cdffc26d7dacf4 (diff) | |
download | klee-b585a94ad0cb30570cf4f14e2dc1ebb43f694bb3.tar.gz |
add declarations to escapingFunctions
Diffstat (limited to 'test')
-rw-r--r-- | test/Feature/EscapingFunctions.c | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/test/Feature/EscapingFunctions.c b/test/Feature/EscapingFunctions.c index 8c9612a5..bb9b8a4a 100644 --- a/test/Feature/EscapingFunctions.c +++ b/test/Feature/EscapingFunctions.c @@ -3,6 +3,8 @@ // 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> + int functionpointer(void) { return 1; } @@ -33,6 +35,9 @@ two: return 2; } +int function_declaration(void); +uint8_t bitcasted_function_declaration(void); + int main(int argc, char *argv[]) { int (*f1)(void) = functionpointer; f1(); @@ -44,6 +49,12 @@ int main(int argc, char *argv[]) { blockaddress(argc); - // CHECK: KLEE: escaping functions: {{\[((functionpointer|functionpointer_as_argument|bitcasted_functionpointer), ){3}\]}} + int (*f3)(void) = function_declaration; + f3(); + + uint64_t (*f4)(void) =(uint64_t (*)(void))bitcasted_function_declaration; + f4(); + + // CHECK: KLEE: escaping functions: {{\[((functionpointer|functionpointer_as_argument|bitcasted_functionpointer|function_declaration|bitcasted_function_declaration), ){5}\]}} return 0; } |