-
Notifications
You must be signed in to change notification settings - Fork 275
Fixed show-call-sequences feature of goto instrument; added test suite #1217
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
int foo(int x){ | ||
if (x==3){ | ||
return 0; | ||
} | ||
else{ | ||
return 3; | ||
} | ||
} | ||
|
||
int main() { | ||
foo(0); | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
CORE | ||
main.c | ||
--show-call-sequences | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ | ||
main -> foo | ||
-- | ||
foo -> foo | ||
main -> main | ||
foo -> main |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,17 @@ | ||
int foo(int x) | ||
{ | ||
if (x==3) | ||
{ | ||
return 0; | ||
} | ||
else | ||
{ | ||
return foo(3); | ||
} | ||
} | ||
|
||
int main() | ||
{ | ||
foo(0); | ||
return 0; | ||
} | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Newline missing |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
CORE | ||
main.c | ||
--show-call-sequences | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ | ||
main -> foo | ||
foo -> foo | ||
-- | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Add the unexpected cases There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. addressed in latest commit |
||
foo -> main | ||
main -> main |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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; | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
CORE | ||
main.c | ||
--show-call-sequences | ||
^SIGNAL=0$ | ||
^EXIT=0$ | ||
recurse -> recurse | ||
recurse -> foo | ||
-- | ||
foo -> foo | ||
foo -> recurse |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,22 @@ | ||
void foo() | ||
{ | ||
moo(); | ||
boo(); | ||
} | ||
|
||
void moo() | ||
{ | ||
return; | ||
} | ||
|
||
void boo() | ||
{ | ||
return; | ||
} | ||
|
||
int main() | ||
{ | ||
moo(); | ||
foo(); | ||
return 0; | ||
} | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Newline missing |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -23,14 +23,15 @@ Date: April 2013 | |
#include <goto-programs/goto_model.h> | ||
|
||
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'; | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Is this output desired? If so, then it should be tested. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. addressed in latest commit by adding new test |
||
std::stack<goto_programt::const_targett> stack; | ||
std::set<goto_programt::const_targett> 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); | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
ideally, test cases should follow coding guidelines too
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
addressed in latest commit