Skip to content

Commit 9d4e0ca

Browse files
authored
Merge pull request diffblue#1217 from KPouliasis/show_functions_dfs
Fixed show-call-sequences feature of goto instrument; added test suite
2 parents c5c77ac + 622e2e3 commit 9d4e0ca

File tree

9 files changed

+138
-47
lines changed

9 files changed

+138
-47
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
int foo(int x){
2+
if (x==3){
3+
return 0;
4+
}
5+
else{
6+
return 3;
7+
}
8+
}
9+
10+
int main() {
11+
foo(0);
12+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--show-call-sequences
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
main -> foo
8+
--
9+
foo -> foo
10+
main -> main
11+
foo -> main
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
int foo(int x)
2+
{
3+
if (x==3)
4+
{
5+
return 0;
6+
}
7+
else
8+
{
9+
return foo(3);
10+
}
11+
}
12+
13+
int main()
14+
{
15+
foo(0);
16+
return 0;
17+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--show-call-sequences
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
main -> foo
8+
foo -> foo
9+
--
10+
foo -> main
11+
main -> main
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
int foo(int x)
2+
{
3+
if (x==3)
4+
{
5+
return 0;
6+
}
7+
else
8+
{
9+
return 3;
10+
}
11+
}
12+
13+
void recurse(int low)
14+
{
15+
if(low >= 2)
16+
{
17+
recurse(low-1);
18+
recurse(low-2);
19+
}
20+
else
21+
{
22+
foo(2);
23+
foo(3);
24+
return;
25+
}
26+
}
27+
28+
int main()
29+
{
30+
recurse(5);
31+
return 0;
32+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--show-call-sequences
4+
^SIGNAL=0$
5+
^EXIT=0$
6+
recurse -> recurse
7+
recurse -> foo
8+
--
9+
foo -> foo
10+
foo -> recurse
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
void foo()
2+
{
3+
moo();
4+
boo();
5+
}
6+
7+
void moo()
8+
{
9+
return;
10+
}
11+
12+
void boo()
13+
{
14+
return;
15+
}
16+
17+
int main()
18+
{
19+
moo();
20+
foo();
21+
return 0;
22+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--show-call-sequences
4+
activate-multi-line-match
5+
main -> moo\nmain -> foo
6+
foo -> moo\nfoo -> boo
7+
SIGNAL=0
8+
EXIT=0
9+
--
10+
main -> boo
11+
boo -> foo
12+
moo -> foo

src/goto-instrument/call_sequences.cpp

+11-47
Original file line numberDiff line numberDiff line change
@@ -23,14 +23,15 @@ Date: April 2013
2323
#include <goto-programs/goto_model.h>
2424

2525
void show_call_sequences(
26-
const irep_idt &function,
27-
const goto_programt &goto_program,
28-
const goto_programt::const_targett start)
26+
const irep_idt &caller,
27+
const goto_programt &goto_program)
2928
{
30-
std::cout << "# From " << function << '\n';
31-
29+
// show calls in blocks within caller body
30+
// dfs on code blocks using stack
31+
std::cout << "# " << caller << '\n';
3232
std::stack<goto_programt::const_targett> stack;
3333
std::set<goto_programt::const_targett> seen;
34+
const goto_programt::const_targett start=goto_program.instructions.begin();
3435

3536
if(start!=goto_program.instructions.end())
3637
stack.push(start);
@@ -42,17 +43,14 @@ void show_call_sequences(
4243

4344
if(!seen.insert(t).second)
4445
continue; // seen it already
45-
4646
if(t->is_function_call())
4747
{
48-
const exprt &function2=to_code_function_call(t->code).function();
49-
if(function2.id()==ID_symbol)
48+
const exprt &callee=to_code_function_call(t->code).function();
49+
if(callee.id()==ID_symbol)
5050
{
51-
// print pair function, function2
52-
std::cout << function << " -> "
53-
<< to_symbol_expr(function2).get_identifier() << '\n';
51+
std::cout << caller << " -> "
52+
<< to_symbol_expr(callee).get_identifier() << '\n';
5453
}
55-
continue; // abort search
5654
}
5755

5856
// get successors and add to stack
@@ -61,47 +59,13 @@ void show_call_sequences(
6159
stack.push(it);
6260
}
6361
}
64-
}
65-
66-
void show_call_sequences(
67-
const irep_idt &function,
68-
const goto_programt &goto_program)
69-
{
70-
// this is quadratic
71-
72-
std::cout << "# " << function << '\n';
73-
74-
show_call_sequences(
75-
function,
76-
goto_program,
77-
goto_program.instructions.begin());
78-
79-
forall_goto_program_instructions(i_it, goto_program)
80-
{
81-
if(!i_it->is_function_call())
82-
continue;
83-
84-
const exprt &f1=to_code_function_call(i_it->code).function();
85-
86-
if(f1.id()!=ID_symbol)
87-
continue;
88-
89-
// find any calls reachable from this one
90-
goto_programt::const_targett next=i_it;
91-
next++;
92-
93-
show_call_sequences(
94-
to_symbol_expr(f1).get_identifier(),
95-
goto_program,
96-
next);
97-
}
98-
9962
std::cout << '\n';
10063
}
10164

10265
void show_call_sequences(const goto_modelt &goto_model)
10366
{
10467
// do per function
68+
// show the calls in the body of the specific function
10569

10670
forall_goto_functions(f_it, goto_model.goto_functions)
10771
show_call_sequences(f_it->first, f_it->second.body);

0 commit comments

Comments
 (0)