diff options
| author | Julian Büning <julian.buening@rwth-aachen.de> | 2018-10-27 22:14:50 +0200 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-05-30 09:45:21 +0100 |
| commit | 3629e3ef0fc999ba9c1e0f43db061bdcc875d735 (patch) | |
| tree | 3f35cecfc8f1139f113b7f2fc76b6a2ba9be9b81 /test/Feature/FunctionAliasExit.c | |
| parent | 4b93a3ecf7514d181730f5a8f8bfe7e086160b4c (diff) | |
| download | klee-3629e3ef0fc999ba9c1e0f43db061bdcc875d735.tar.gz | |
implement FunctionAliasPass
Diffstat (limited to 'test/Feature/FunctionAliasExit.c')
| -rw-r--r-- | test/Feature/FunctionAliasExit.c | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/test/Feature/FunctionAliasExit.c b/test/Feature/FunctionAliasExit.c new file mode 100644 index 00000000..b30838d0 --- /dev/null +++ b/test/Feature/FunctionAliasExit.c @@ -0,0 +1,31 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -function-alias=exit:end %t.bc 2>&1 | FileCheck %s + +#include <stdio.h> +#include <stdlib.h> +#include <unistd.h> + +// CHECK: KLEE: function-alias: replaced @exit with @end + +void start(int x) { + // CHECK: START + printf("START\n"); + if (x == 53) + // CHECK: END: status = 1 + exit(1); +} + +void __attribute__ ((noinline)) end(int status) { + printf("END: status = %d\n", status); + klee_silent_exit(status); +} + +int main() { + int x; + klee_make_symbolic(&x, sizeof(x), "x"); + + start(x); + // CHECK: END: status = 0 + end(0); +} |
