File tree Expand file tree Collapse file tree 4 files changed +202
-0
lines changed
regression/goto-instrument Expand file tree Collapse file tree 4 files changed +202
-0
lines changed Original file line number Diff line number Diff line change 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+ }
Original file line number Diff line number Diff line change 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
Original file line number Diff line number Diff line change 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+ }
Original file line number Diff line number Diff line change 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
You can’t perform that action at this time.
0 commit comments