diff --git a/regression/goto-instrument/show-call-sequences1/main.c b/regression/goto-instrument/show-call-sequences1/main.c new file mode 100644 index 00000000000..40fc500ff47 --- /dev/null +++ b/regression/goto-instrument/show-call-sequences1/main.c @@ -0,0 +1,12 @@ +int foo(int x){ + if (x==3){ + return 0; + } + else{ + return 3; + } +} + +int main() { + foo(0); +} diff --git a/regression/goto-instrument/show-call-sequences1/test.desc b/regression/goto-instrument/show-call-sequences1/test.desc new file mode 100644 index 00000000000..67687f93b54 --- /dev/null +++ b/regression/goto-instrument/show-call-sequences1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--show-call-sequences +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +main -> foo +-- +foo -> foo +main -> main +foo -> main diff --git a/regression/goto-instrument/show-call-sequences2/main.c b/regression/goto-instrument/show-call-sequences2/main.c new file mode 100644 index 00000000000..2def1f29d87 --- /dev/null +++ b/regression/goto-instrument/show-call-sequences2/main.c @@ -0,0 +1,17 @@ +int foo(int x) +{ + if (x==3) + { + return 0; + } + else + { + return foo(3); + } +} + +int main() +{ + foo(0); + return 0; +} \ No newline at end of file diff --git a/regression/goto-instrument/show-call-sequences2/test.desc b/regression/goto-instrument/show-call-sequences2/test.desc new file mode 100644 index 00000000000..0664a51f89c --- /dev/null +++ b/regression/goto-instrument/show-call-sequences2/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--show-call-sequences +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +main -> foo +foo -> foo +-- +foo -> main +main -> main diff --git a/regression/goto-instrument/show-call-sequences3/main.c b/regression/goto-instrument/show-call-sequences3/main.c new file mode 100644 index 00000000000..77b86241734 --- /dev/null +++ b/regression/goto-instrument/show-call-sequences3/main.c @@ -0,0 +1,32 @@ +int foo(int x) +{ + if (x==3) + { + return 0; + } + else + { + return 3; + } +} + +void recurse(int low) +{ + if(low >= 2) + { + recurse(low-1); + recurse(low-2); + } + else + { + foo(2); + foo(3); + return; + } +} + +int main() +{ + recurse(5); + return 0; +} diff --git a/regression/goto-instrument/show-call-sequences3/test.desc b/regression/goto-instrument/show-call-sequences3/test.desc new file mode 100644 index 00000000000..3649ff2e097 --- /dev/null +++ b/regression/goto-instrument/show-call-sequences3/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--show-call-sequences +^SIGNAL=0$ +^EXIT=0$ +recurse -> recurse +recurse -> foo +-- +foo -> foo +foo -> recurse diff --git a/regression/goto-instrument/show-call-sequences4/main.c b/regression/goto-instrument/show-call-sequences4/main.c new file mode 100644 index 00000000000..80ed2c3b5e0 --- /dev/null +++ b/regression/goto-instrument/show-call-sequences4/main.c @@ -0,0 +1,22 @@ +void foo() +{ + moo(); + boo(); +} + +void moo() +{ + return; +} + +void boo() +{ + return; +} + +int main() +{ + moo(); + foo(); + return 0; +} \ No newline at end of file diff --git a/regression/goto-instrument/show-call-sequences4/test.desc b/regression/goto-instrument/show-call-sequences4/test.desc new file mode 100644 index 00000000000..c5dec9dcb70 --- /dev/null +++ b/regression/goto-instrument/show-call-sequences4/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--show-call-sequences +activate-multi-line-match +main -> moo\nmain -> foo +foo -> moo\nfoo -> boo +SIGNAL=0 +EXIT=0 +-- +main -> boo +boo -> foo +moo -> foo diff --git a/src/goto-instrument/call_sequences.cpp b/src/goto-instrument/call_sequences.cpp index 29236975364..cc16768f870 100644 --- a/src/goto-instrument/call_sequences.cpp +++ b/src/goto-instrument/call_sequences.cpp @@ -23,14 +23,15 @@ Date: April 2013 #include void show_call_sequences( - const irep_idt &function, - const goto_programt &goto_program, - const goto_programt::const_targett start) + const irep_idt &caller, + const goto_programt &goto_program) { - std::cout << "# From " << function << '\n'; - + // show calls in blocks within caller body + // dfs on code blocks using stack + std::cout << "# " << caller << '\n'; std::stack stack; std::set seen; + const goto_programt::const_targett start=goto_program.instructions.begin(); if(start!=goto_program.instructions.end()) stack.push(start); @@ -42,17 +43,14 @@ void show_call_sequences( if(!seen.insert(t).second) continue; // seen it already - if(t->is_function_call()) { - const exprt &function2=to_code_function_call(t->code).function(); - if(function2.id()==ID_symbol) + const exprt &callee=to_code_function_call(t->code).function(); + if(callee.id()==ID_symbol) { - // print pair function, function2 - std::cout << function << " -> " - << to_symbol_expr(function2).get_identifier() << '\n'; + std::cout << caller << " -> " + << to_symbol_expr(callee).get_identifier() << '\n'; } - continue; // abort search } // get successors and add to stack @@ -61,47 +59,13 @@ void show_call_sequences( stack.push(it); } } -} - -void show_call_sequences( - const irep_idt &function, - const goto_programt &goto_program) -{ - // this is quadratic - - std::cout << "# " << function << '\n'; - - show_call_sequences( - function, - goto_program, - goto_program.instructions.begin()); - - forall_goto_program_instructions(i_it, goto_program) - { - if(!i_it->is_function_call()) - continue; - - const exprt &f1=to_code_function_call(i_it->code).function(); - - if(f1.id()!=ID_symbol) - continue; - - // find any calls reachable from this one - goto_programt::const_targett next=i_it; - next++; - - show_call_sequences( - to_symbol_expr(f1).get_identifier(), - goto_program, - next); - } - std::cout << '\n'; } void show_call_sequences(const goto_modelt &goto_model) { // do per function + // show the calls in the body of the specific function forall_goto_functions(f_it, goto_model.goto_functions) show_call_sequences(f_it->first, f_it->second.body);