diff options
author | Felix Rath <felix.rath@comsys.rwth-aachen.de> | 2020-05-22 14:09:10 +0200 |
---|---|---|
committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2020-10-12 11:19:24 +0100 |
commit | c09306ffd894f95be195723327d5b17dca73ebd1 (patch) | |
tree | 592773383280012bce8856b28503ab61de0deb98 /test/CXX/symex/basic_c++ | |
parent | d920e049fa955877f772188fdc58cab1b31aabc9 (diff) | |
download | klee-c09306ffd894f95be195723327d5b17dca73ebd1.tar.gz |
Implemented support for C++ Exceptions
We implement the Itanium ABI unwinding base-API, and leave the C++-specific parts to libcxxabi. Co-authored-by: Lukas Wölfer <lukas.woelfer@rwth-aachen.de>
Diffstat (limited to 'test/CXX/symex/basic_c++')
-rw-r--r-- | test/CXX/symex/basic_c++/diamond.cpp | 45 | ||||
-rw-r--r-- | test/CXX/symex/basic_c++/inheritance.cpp | 35 | ||||
-rw-r--r-- | test/CXX/symex/basic_c++/lambda.cpp | 20 | ||||
-rw-r--r-- | test/CXX/symex/basic_c++/namespace.cpp | 18 | ||||
-rw-r--r-- | test/CXX/symex/basic_c++/reinterpret_cast.cpp | 26 | ||||
-rw-r--r-- | test/CXX/symex/basic_c++/simple.cpp | 33 | ||||
-rw-r--r-- | test/CXX/symex/basic_c++/templates.cpp | 28 | ||||
-rw-r--r-- | test/CXX/symex/basic_c++/virtual.cpp | 35 |
8 files changed, 240 insertions, 0 deletions
diff --git a/test/CXX/symex/basic_c++/diamond.cpp b/test/CXX/symex/basic_c++/diamond.cpp new file mode 100644 index 00000000..479a9090 --- /dev/null +++ b/test/CXX/symex/basic_c++/diamond.cpp @@ -0,0 +1,45 @@ +// REQUIRES: uclibc +// RUN: %clangxx %s -emit-llvm %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --libc=uclibc %t.bc 2>&1 | FileCheck %s + +#include <cstdio> + +struct A { + int a; + A() { + printf("A constructor\n"); + } +}; + +struct B : virtual A { + int b; + B() { + printf("B constructor\n"); + } +}; + +struct C : virtual A { + int c; + C() { + printf("C constructor\n"); + } +}; + +struct D : B, C { + int d; +}; + +int main(int argc, char **args) { + D x; + // CHECK: A constructor + // CHECK: B constructor + // CHECK: C constructor + + x.a = 7; + B *y = &x; + printf("B::a = %d\n", y->a); + // CHECK: B::a = 7 + + return 0; +} diff --git a/test/CXX/symex/basic_c++/inheritance.cpp b/test/CXX/symex/basic_c++/inheritance.cpp new file mode 100644 index 00000000..88a0d150 --- /dev/null +++ b/test/CXX/symex/basic_c++/inheritance.cpp @@ -0,0 +1,35 @@ +// REQUIRES: uclibc +// RUN: %clangxx %s -emit-llvm %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --libc=uclibc %t.bc 2>&1 | FileCheck %s + +#include <cstdio> +class Testclass { +public: + Testclass() { + printf("Testclass constructor\n"); + } + int a() { + return 1; + } +}; +class Derivedclass : public Testclass { +public: + Derivedclass() { + printf("Derivedclass constructor\n"); + } + int b() { + return 2; + } +}; + +int main(int argc, char **args) { + Derivedclass x; + // CHECK: Testclass constructor + // CHECK: Derivedclass constructor + + printf("%d / %d", x.a(), x.b()); + // CHECK: 1 / 2 + + return x.a() + x.b(); +} diff --git a/test/CXX/symex/basic_c++/lambda.cpp b/test/CXX/symex/basic_c++/lambda.cpp new file mode 100644 index 00000000..e7f8f971 --- /dev/null +++ b/test/CXX/symex/basic_c++/lambda.cpp @@ -0,0 +1,20 @@ +// REQUIRES: uclibc +// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --libc=uclibc %t.bc 2>&1 | FileCheck %s + +#include <cstdio> + +int main(int argc, char **args) { + int x = 0; + auto y = [&](int h) { return x + h; }; + auto z = [=](int h) { return x + h; }; + x = 1; + + printf("y(0) == %d\n", y(0)); + // CHECK: y(0) == 1 + printf("z(0) == %d\n", z(0)); + // CHECK: z(0) == 0 + + return 0; +} diff --git a/test/CXX/symex/basic_c++/namespace.cpp b/test/CXX/symex/basic_c++/namespace.cpp new file mode 100644 index 00000000..939e9bcd --- /dev/null +++ b/test/CXX/symex/basic_c++/namespace.cpp @@ -0,0 +1,18 @@ +// REQUIRES: uclibc +// RUN: %clangxx %s -emit-llvm %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --libc=uclibc %t.bc 2>&1 | FileCheck %s + +#include <cstdio> + +namespace test { +int a() { + return 2; +} +} // namespace test + +int main(int argc, char **args) { + printf("test::a() == %d\n", test::a()); + //CHECK: test::a() == 2 + return 0; +} diff --git a/test/CXX/symex/basic_c++/reinterpret_cast.cpp b/test/CXX/symex/basic_c++/reinterpret_cast.cpp new file mode 100644 index 00000000..6883226b --- /dev/null +++ b/test/CXX/symex/basic_c++/reinterpret_cast.cpp @@ -0,0 +1,26 @@ +// REQUIRES: uclibc +// RUN: %clangxx %s -emit-llvm %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --libc=uclibc %t.bc 2>&1 | FileCheck %s + +#include <cstdio> + +int main(int argc, char **args) { + unsigned int *x = new unsigned int(0); + char *y = reinterpret_cast<char *>(x); + + printf("address(x) == %p\n", x); + printf("address(y) == %p\n", y); + // CHECK: address(x) == [[POINTER_X:0x[a-fA-F0-9]+]] + // CHECK: address(y) == [[POINTER_X]] + + printf("first x == 0x%08X\n", *x); + // CHECK: first x == 0x00000000 + y[3] = 0xAB; + y[1] = 0x78; + printf("second x == 0x%08X\n", *x); + // CHECK: second x == 0xAB007800 + + delete x; + return 0; +} diff --git a/test/CXX/symex/basic_c++/simple.cpp b/test/CXX/symex/basic_c++/simple.cpp new file mode 100644 index 00000000..f66dbd1e --- /dev/null +++ b/test/CXX/symex/basic_c++/simple.cpp @@ -0,0 +1,33 @@ +// REQUIRES: uclibc +// RUN: %clangxx %s -emit-llvm %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --libc=uclibc %t.bc 2>&1 | FileCheck %s + +// CHECK: KLEE: done: completed paths = 5 + +#include "klee/klee.h" + +class Test { + int x; + +public: + Test(int _x) : x(_x) {} + + int test() { + if (x % 2 == 0) + return 0; + if (x % 3 == 0) + return 1; + if (x % 5 == 0) + return 2; + if (x % 7 == 0) + return 3; + return 4; + } +}; + +int main(int argc, char **args) { + Test a(klee_int("Test")); + + return a.test(); +} diff --git a/test/CXX/symex/basic_c++/templates.cpp b/test/CXX/symex/basic_c++/templates.cpp new file mode 100644 index 00000000..c5abb983 --- /dev/null +++ b/test/CXX/symex/basic_c++/templates.cpp @@ -0,0 +1,28 @@ +// REQUIRES: uclibc +// RUN: %clangxx %s -emit-llvm %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --libc=uclibc %t.bc 2>&1 + +#include <cassert> + +template <typename X, typename Y> +X multiply(X a, Y b) { + return a * b; +} + +template <int A> +int add(int summand) { + return A + summand; +} + +int main(int argc, char **args) { + assert(add<7>(3) == 10); + + assert(multiply(7, 3) == 21); + + // Check if the float arguments are handled correctly + assert(multiply(7.1f, 3) > 21); + assert(multiply(3, 7.1f) == 21); + + return 0; +} diff --git a/test/CXX/symex/basic_c++/virtual.cpp b/test/CXX/symex/basic_c++/virtual.cpp new file mode 100644 index 00000000..b4850992 --- /dev/null +++ b/test/CXX/symex/basic_c++/virtual.cpp @@ -0,0 +1,35 @@ +// REQUIRES: uclibc +// RUN: %clangxx %s -emit-llvm %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --libc=uclibc %t.bc 2>&1 + +#include <cassert> + +class Testclass { +public: + virtual int vtl() { + return 1; + } +}; + +class Derivedclass : public Testclass { +}; + +class Overridingclass : public Derivedclass { +public: + int vtl() override { + return 2; + } +}; + +int main(int argc, char **args) { + Testclass x; + Derivedclass y; + Overridingclass z; + + assert(x.vtl() == 1); + assert(y.vtl() == 1); + assert(z.vtl() == 2); + + return 0; +} |