Skip to content

Commit 5f9b2d7

Browse files
committed
C2PO: Fix test case to incur no warnings, besides for __goblint_check.
1 parent cd52bde commit 5f9b2d7

File tree

1 file changed

+29
-10
lines changed

1 file changed

+29
-10
lines changed
Lines changed: 29 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,35 @@
11
// PARAM: --set ana.activated[+] c2po --set ana.activated[+] startState --set ana.activated[+] taintPartialContexts --set ana.c2po.askbase false
2-
int a, b, c;
3-
void *d(const *e) { return e + 200; }
4-
int *f() {}
5-
main() {
6-
g(a, c, b);
7-
if (0) {
8-
__goblint_check(0); // NOWARN (unreachable)
9-
}
10-
__goblint_check(1); // reachable
2+
int a;
3+
4+
struct h {
5+
int c;
6+
};
7+
8+
struct i {
9+
int d;
10+
};
11+
12+
struct h* b;
13+
struct i* c;
14+
15+
const void *d(const int* e) {
16+
return e + 200;
17+
}
18+
19+
int *f() {
20+
return (int*) 0;
1121
}
12-
g(int, struct h *, struct i *) {
22+
23+
int g(int, struct h *, struct i *) {
1324
int *j = f();
1425
d(j);
1526
__goblint_check(1); // reachable
1627
}
28+
29+
int main() {
30+
g(a, b, c);
31+
if (0) {
32+
__goblint_check(0); // NOWARN (unreachable)
33+
}
34+
__goblint_check(1); // reachable
35+
}

0 commit comments

Comments
 (0)