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
|
// test exception handling
extern "C" {
extern void __ikos_assert(int) noexcept;
extern int __ikos_nondet_int(void) noexcept;
}
int x;
int y;
int f() {
x = 0;
y = 0;
try {
if (__ikos_nondet_int()) {
x = 1;
throw 0x42;
} else if (__ikos_nondet_int()) {
return 0;
}
} catch (int) {
__ikos_assert(x == 1);
if (__ikos_nondet_int()) {
y = 1;
throw 0x42;
} else {
return 1;
}
}
return 2;
}
int main() {
try {
int r = f();
__ikos_assert(r >= 0 && r <= 2); // ok
__ikos_assert(x >= 0 && x <= 1); // ok
__ikos_assert(y == 0); // ok
} catch (int) {
__ikos_assert(x == 1); // ok
__ikos_assert(y == 1); // warning because ikos is imprecise on the type of
// exception. The first catch() {...} catches all exceptions and rethrow
// the exception if it does not have the type void*.
}
return 0;
}
|
