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 | |
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')
-rw-r--r-- | test/Feature/EntryPoint.c | 10 | ||||
-rw-r--r-- | test/Feature/EntryPointMissing.c | 64 | ||||
-rw-r--r-- | test/Feature/EntryPointUclibcPosix.c | 45 |
3 files changed, 119 insertions, 0 deletions
diff --git a/test/Feature/EntryPoint.c b/test/Feature/EntryPoint.c index 8a10d36f..48442659 100644 --- a/test/Feature/EntryPoint.c +++ b/test/Feature/EntryPoint.c @@ -3,6 +3,10 @@ // RUN: %klee --output-dir=%t.klee-out --entry-point=other_main %t.bc | FileCheck -check-prefix=CHECK-OTHER_MAIN %s // RUN: rm -rf %t.klee-out +// RUN: %clang -emit-llvm -g -c -DMAIN %s -o %t.bc +// RUN: %klee --output-dir=%t.klee-out --entry-point=other_main %t.bc | FileCheck -check-prefix=CHECK-OTHER_MAIN %s + +// RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --entry-point="" %t.bc 2>%t.stderr.log || echo "Exit status must be 0" // RUN: FileCheck -check-prefix=CHECK-EMPTY --input-file=%t.stderr.log %s @@ -14,4 +18,10 @@ int other_main() { return 0; } +#ifdef MAIN +int main() { + return 0; +} +#endif + // CHECK-EMPTY: KLEE: ERROR: entry-point cannot be empty 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 diff --git a/test/Feature/EntryPointUclibcPosix.c b/test/Feature/EntryPointUclibcPosix.c new file mode 100644 index 00000000..e3d80928 --- /dev/null +++ b/test/Feature/EntryPointUclibcPosix.c @@ -0,0 +1,45 @@ +// REQUIRES: uclibc +// REQUIRES: posix-runtime + +/* Similar test as EntryPoint.c, but with POSIX and uclibc. This + checks that the various wrappers and renames introduced when + linking the uclibc and the POSIX runtime are correctly handled. */ + +// RUN: %clang -emit-llvm -g -c %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --libc=uclibc --posix-runtime --output-dir=%t.klee-out --entry-point=other_main %t.bc | FileCheck %s + +// RUN: rm -rf %t.klee-out +// RUN: %clang -emit-llvm -g -c -DMAIN %s -o %t.bc +// RUN: %klee --libc=uclibc --posix-runtime --output-dir=%t.klee-out --entry-point=other_main %t.bc | FileCheck %s + +// RUN: %clang -emit-llvm -g -c %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --libc=uclibc --output-dir=%t.klee-out --entry-point=other_main %t.bc | FileCheck %s + +// RUN: rm -rf %t.klee-out +// RUN: %clang -emit-llvm -g -c -DMAIN %s -o %t.bc +// RUN: %klee --libc=uclibc --output-dir=%t.klee-out --entry-point=other_main %t.bc | FileCheck %s + +// RUN: %clang -emit-llvm -g -c %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --posix-runtime --output-dir=%t.klee-out --entry-point=other_main %t.bc | FileCheck %s + +// RUN: rm -rf %t.klee-out +// RUN: %clang -emit-llvm -g -c -DMAIN %s -o %t.bc +// RUN: %klee --posix-runtime --output-dir=%t.klee-out --entry-point=other_main %t.bc | FileCheck %s + + +#include <stdio.h> + +int other_main() { + printf("Hello World\n"); + // CHECK: Hello World + return 0; +} + +#ifdef MAIN +int main() { + return 0; +} +#endif |