From 94376216f09802dd1d402b317dd703071e9a7099 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <c.cadar@imperial.ac.uk>
Date: Tue, 21 Mar 2023 17:19:14 +0000
Subject: Added more test cases for --entry-point. EntryPointMissing is
 currently expected to fail.

---
 test/Feature/EntryPoint.c            | 10 ++++++
 test/Feature/EntryPointMissing.c     | 64 ++++++++++++++++++++++++++++++++++++
 test/Feature/EntryPointUclibcPosix.c | 45 +++++++++++++++++++++++++
 3 files changed, 119 insertions(+)
 create mode 100644 test/Feature/EntryPointMissing.c
 create mode 100644 test/Feature/EntryPointUclibcPosix.c

(limited to 'test')

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
@@ -2,6 +2,10 @@
 // RUN: rm -rf %t.klee-out
 // 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
-- 
cgit 1.4.1