blob: ab8d7a5c1bfbb9eecb27d108cec4dc030cb48c70 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
// REQUIRES: not-msan
// Disabling msan because it times out on CI
// REQUIRES: libcxx
// REQUIRES: eh-cxx
// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 %libcxx_includes -g -nostdinc++ -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s
#include "klee/klee.h"
#include <cassert>
#include <cstdio>
struct CustomStruct {
int a;
};
int thrower(int x) {
if (x == 0) {
CustomStruct p;
throw p;
} else if (x == 1) {
throw 7;
} else {
throw new CustomStruct();
}
}
int rethrower(int x) {
thrower(x);
return 7;
}
int failed_catch(int x) {
try {
rethrower(x);
} catch (char *ex) {
// Don't catch wrong type
assert(0);
}
// rethrower always throws, cannot reach this instruction
assert(0);
return 0;
}
int catcher(int x) {
try {
failed_catch(x);
} catch (int ex) {
printf("Caught int\n");
// CHECK-DAG: Caught int
return 1;
} catch (CustomStruct ex) {
printf("Caught normal CustomStruct\n");
// CHECK-DAG: Caught normal CustomStruct
return 2;
} catch (CustomStruct *ex) {
printf("Caught pointer CustomStruct\n");
// CHECK-DAG: Caught pointer CustomStruct
return 3;
}
// Unreachable instruction
assert(0);
return 0;
}
int main(int argc, char **args) {
int x = klee_int("x");
int res = catcher(x);
return res;
}
// CHECK-DAG: KLEE: done: completed paths = 3
|
