Skip to content

Commit 0cfc72f

Browse files
author
Owen Jones
committed
Test --call-graph and --reachable-call-graph
Make sure that changes to call_grapht do not alter these two options to goto-instrument
1 parent 3e2ab6f commit 0cfc72f

File tree

4 files changed

+202
-0
lines changed

4 files changed

+202
-0
lines changed
Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
2+
int x;
3+
4+
void func0()
5+
{
6+
func0();
7+
}
8+
9+
void func1()
10+
{
11+
x = 1;
12+
}
13+
14+
void func2()
15+
{
16+
x = 2;
17+
func3();
18+
}
19+
20+
void func3()
21+
{
22+
x = 3;
23+
}
24+
25+
void func4(int b)
26+
{
27+
x = 4;
28+
if(b)
29+
{
30+
func5(0);
31+
}
32+
}
33+
34+
void func5(int b)
35+
{
36+
x = 5;
37+
func4(b);
38+
}
39+
40+
void func6()
41+
{
42+
x = 6;
43+
}
44+
45+
void func7(int b)
46+
{
47+
x = 7;
48+
if(b)
49+
{
50+
func8(0);
51+
}
52+
}
53+
54+
void func8(int b)
55+
{
56+
x = 8;
57+
func7(b);
58+
}
59+
60+
void func9()
61+
{
62+
x = 9;
63+
funca();
64+
}
65+
66+
void funca()
67+
{
68+
x = 10;
69+
func9();
70+
}
71+
72+
73+
74+
int main()
75+
{
76+
func1();
77+
func2();
78+
func4(1);
79+
80+
return 0;
81+
}
Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE
2+
main.c
3+
--call-graph
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main -> func2$
7+
^main -> func1$
8+
^main -> func4$
9+
^funca -> func9$
10+
^func9 -> funca$
11+
^func8 -> func7$
12+
^func7 -> func8$
13+
^__CPROVER__start -> __CPROVER_initialize$
14+
^__CPROVER__start -> main$
15+
^func2 -> func3$
16+
^func0 -> func0$
17+
^func4 -> func5$
18+
^func5 -> func4$
19+
--
20+
^warning: ignoring
Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
2+
int x;
3+
4+
void func0()
5+
{
6+
func0();
7+
}
8+
9+
void func1()
10+
{
11+
x = 1;
12+
}
13+
14+
void func2()
15+
{
16+
x = 2;
17+
func3();
18+
}
19+
20+
void func3()
21+
{
22+
x = 3;
23+
}
24+
25+
void func4(int b)
26+
{
27+
x = 4;
28+
if(b)
29+
{
30+
func5(0);
31+
}
32+
}
33+
34+
void func5(int b)
35+
{
36+
x = 5;
37+
func4(b);
38+
}
39+
40+
void func6()
41+
{
42+
x = 6;
43+
}
44+
45+
void func7(int b)
46+
{
47+
x = 7;
48+
if(b)
49+
{
50+
func8(0);
51+
}
52+
}
53+
54+
void func8(int b)
55+
{
56+
x = 8;
57+
func7(b);
58+
}
59+
60+
void func9()
61+
{
62+
x = 9;
63+
funca();
64+
}
65+
66+
void funca()
67+
{
68+
x = 10;
69+
func9();
70+
}
71+
72+
73+
74+
int main()
75+
{
76+
func1();
77+
func2();
78+
func4(1);
79+
80+
return 0;
81+
}
Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE
2+
main.c
3+
--reachable-call-graph
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main -> func2$
7+
^main -> func1$
8+
^main -> func4$
9+
^__CPROVER__start -> __CPROVER_initialize$
10+
^__CPROVER__start -> main$
11+
^func2 -> func3$
12+
^func4 -> func5$
13+
^func5 -> func4$
14+
--
15+
^funca -> func9$
16+
^func9 -> funca$
17+
^func8 -> func7$
18+
^func7 -> func8$
19+
^func0 -> func0$
20+
^warning: ignoring

0 commit comments

Comments
 (0)