diff options
| author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-03-21 17:19:14 +0000 |
|---|---|---|
| committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2023-03-22 22:35:50 +0000 |
| commit | 94376216f09802dd1d402b317dd703071e9a7099 (patch) | |
| tree | 9b6b3d90e121db6421eb4b0f801aeca6a19b8cbd /test/Feature/EntryPointMissing.c | |
| parent | a52050202a53161615e1d088e61ff19d82aeef50 (diff) | |
| download | klee-94376216f09802dd1d402b317dd703071e9a7099.tar.gz | |
Added more test cases for --entry-point. EntryPointMissing is currently expected to fail.
Diffstat (limited to 'test/Feature/EntryPointMissing.c')
| -rw-r--r-- | test/Feature/EntryPointMissing.c | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/test/Feature/EntryPointMissing.c b/test/Feature/EntryPointMissing.c new file mode 100644 index 00000000..3a0d0530 --- /dev/null +++ b/test/Feature/EntryPointMissing.c @@ -0,0 +1,64 @@ +// REQUIRES: posix-runtime +// REQUIRES: uclibc +// XFAIL: * + +// RUN: %clang -emit-llvm -g -c %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out --entry-point=missing %t.bc 2>&1 | FileCheck -check-prefix=CHECK-MISSING %s + +// RUN: %clang -emit-llvm -g -c %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out --entry-point=missing --libc=uclibc %t.bc 2>&1 | FileCheck -check-prefix=CHECK-MISSING %s + +// RUN: %clang -emit-llvm -g -c %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out --entry-point=missing %t.bc --posix-runtime 2>&1 | FileCheck -check-prefix=CHECK-MISSING %s + +// RUN: %clang -emit-llvm -g -c %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out --entry-point=missing %t.bc --libc=uclibc --posix-runtime 2>&1 | FileCheck -check-prefix=CHECK-MISSING %s + +// RUN: %clang -emit-llvm -g -c %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out --entry-point=missing --libc=klee %t.bc 2>&1 | FileCheck -check-prefix=CHECK-MISSING %s + +// RUN: %clang -emit-llvm -g -c %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out --entry-point=missing --libc=klee --posix-runtime %t.bc 2>&1 | FileCheck -check-prefix=CHECK-MISSING %s + + +/* Missing main */ + +// RUN: %clang -emit-llvm -g -c %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out --entry-point=main %t.bc 2>&1 | FileCheck -check-prefix=CHECK-MAIN %s + +// RUN: %clang -emit-llvm -g -c %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out --entry-point=main --libc=uclibc %t.bc 2>&1 | FileCheck -check-prefix=CHECK-MAIN %s + +// RUN: %clang -emit-llvm -g -c %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out --entry-point=main --posix-runtime %t.bc 2>&1 | FileCheck -check-prefix=CHECK-MAIN %s + +// RUN: %clang -emit-llvm -g -c %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out --entry-point=main --libc=uclibc --posix-runtime %t.bc 2>&1 | FileCheck -check-prefix=CHECK-MAIN %s + +// RUN: %clang -emit-llvm -g -c %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out --entry-point=main --libc=klee %t.bc 2>&1 | FileCheck -check-prefix=CHECK-MAIN %s + +// RUN: %clang -emit-llvm -g -c %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out --entry-point=main --libc=klee --posix-runtime %t.bc 2>&1 | FileCheck -check-prefix=CHECK-MAIN %s + +#include <stdio.h> + +int hello() { + printf("Hello World\n"); + return 0; +} + +// CHECK-MISSING: Entry function 'missing' not found in module +// CHECK-MAIN: Entry function 'main' not found in module |