From 1fab1c1f657a9a434b7187be6adc779b94d59401 Mon Sep 17 00:00:00 2001 From: kpouliasis Date: Mon, 7 Aug 2017 11:41:08 -0400 Subject: [PATCH] Fixed show-call-sequences deature of goto instrument; added test suite --- .../show-call-sequences1/main.c | 12 ++++ .../show-call-sequences1/test.desc | 11 ++++ .../show-call-sequences2/main.c | 17 +++++ .../show-call-sequences2/test.desc | 11 ++++ .../show-call-sequences3/main.c | 32 ++++++++++ .../show-call-sequences3/test.desc | 10 +++ .../show-call-sequences4/main.c | 22 +++++++ .../show-call-sequences4/test.desc | 12 ++++ src/goto-instrument/call_sequences.cpp | 62 ++++--------------- 9 files changed, 139 insertions(+), 50 deletions(-) create mode 100644 regression/goto-instrument/show-call-sequences1/main.c create mode 100644 regression/goto-instrument/show-call-sequences1/test.desc create mode 100644 regression/goto-instrument/show-call-sequences2/main.c create mode 100644 regression/goto-instrument/show-call-sequences2/test.desc create mode 100644 regression/goto-instrument/show-call-sequences3/main.c create mode 100644 regression/goto-instrument/show-call-sequences3/test.desc create mode 100644 regression/goto-instrument/show-call-sequences4/main.c create mode 100644 regression/goto-instrument/show-call-sequences4/test.desc 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 7c8ed65a918..6022244911a 100644 --- a/src/goto-instrument/call_sequences.cpp +++ b/src/goto-instrument/call_sequences.cpp @@ -21,14 +21,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); @@ -40,17 +41,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 @@ -59,52 +57,16 @@ 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_functionst &goto_functions) { // do per function - + // show the calls in the body of the specific function forall_goto_functions(f_it, goto_functions) show_call_sequences(f_it->first, f_it->second.body); -} +} class check_call_sequencet { public: