diff --git a/regression/cbmc/trace_show_code/main.c b/regression/cbmc/trace_show_code/main.c new file mode 100644 index 00000000000..d725e9d0c22 --- /dev/null +++ b/regression/cbmc/trace_show_code/main.c @@ -0,0 +1,23 @@ +int function_to_call(int a) +{ + int local = 1; + return a+local; +} + + +int main() +{ + int a, c; + unsigned int b; + a = 0; + c = -100; + a = function_to_call(a) + function_to_call(c); + if(a < 0) + b = function_to_call(b); + + if(c < 0) + b = -function_to_call(b); + + __CPROVER_assert(0,""); + +} diff --git a/regression/cbmc/trace_show_code/test.desc b/regression/cbmc/trace_show_code/test.desc new file mode 100644 index 00000000000..962278e6598 --- /dev/null +++ b/regression/cbmc/trace_show_code/test.desc @@ -0,0 +1,19 @@ +CORE +main.c +--trace --trace-show-code +^EXIT=10$ +^SIGNAL=0$ +local = 1 +int a +int c +unsigned int b +a = 0; +c = -100; +function_to_call\(a\) +function_to_call\(c\) +a = return_value_function_to_call \+ return_value_function_to_call +function_to_call\(\(signed int\)b\) +b = \(unsigned int\)return_value_function_to_call +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc/trace_show_function_calls/main.c b/regression/cbmc/trace_show_function_calls/main.c new file mode 100644 index 00000000000..bb1ca004bc6 --- /dev/null +++ b/regression/cbmc/trace_show_function_calls/main.c @@ -0,0 +1,22 @@ +int function_to_call(int a) +{ + int local = 1; + return a+local; +} + + +int main() +{ + int a; + unsigned int b; + a = 0; + a = -100; + a = 2147483647; + b = a*2; + a = -2147483647; + a = function_to_call(a); + b = function_to_call(b); + + __CPROVER_assert(0,""); + +} diff --git a/regression/cbmc/trace_show_function_calls/test.desc b/regression/cbmc/trace_show_function_calls/test.desc new file mode 100644 index 00000000000..d4d92b0cfda --- /dev/null +++ b/regression/cbmc/trace_show_function_calls/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--trace --trace-show-function-calls +^EXIT=10$ +^SIGNAL=0$ +Function call: function_to_call \(depth 2\) +Function return: function_to_call \(depth 1\) +Function call: function_to_call \(depth 2\) +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 5243dbf0cf7..1416b20dc57 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -247,20 +247,30 @@ void trace_value( void show_state_header( std::ostream &out, + const namespacet &ns, const goto_trace_stept &state, const source_locationt &source_location, - unsigned step_nr) + unsigned step_nr, + const trace_optionst &options) { out << "\n"; - if(step_nr==0) + if(step_nr == 0) out << "Initial State"; else out << "State " << step_nr; - out << " " << source_location - << " thread " << state.thread_nr << "\n"; - out << "----------------------------------------------------" << "\n"; + out << " " << source_location << " thread " << state.thread_nr << "\n"; + out << "----------------------------------------------------" + << "\n"; + + if(options.show_code) + { + out << as_string(ns, *state.pc) + << "\n"; + out << "----------------------------------------------------" + << "\n"; + } } bool is_index_member_symbol(const exprt &src) @@ -283,6 +293,7 @@ void show_goto_trace( { unsigned prev_step_nr=0; bool first_step=true; + std::size_t function_depth=0; for(const auto &step : goto_trace.steps) { @@ -341,7 +352,8 @@ void show_goto_trace( { first_step=false; prev_step_nr=step.step_nr; - show_state_header(out, step, step.pc->source_location, step.step_nr); + show_state_header( + out, ns, step, step.pc->source_location, step.step_nr, options); } // see if the full lhs is something clean @@ -369,7 +381,8 @@ void show_goto_trace( { first_step=false; prev_step_nr=step.step_nr; - show_state_header(out, step, step.pc->source_location, step.step_nr); + show_state_header( + out, ns, step, step.pc->source_location, step.step_nr, options); } trace_value( @@ -386,7 +399,8 @@ void show_goto_trace( } else { - show_state_header(out, step, step.pc->source_location, step.step_nr); + show_state_header( + out, ns, step, step.pc->source_location, step.step_nr, options); out << " OUTPUT " << step.io_id << ":"; for(std::list::const_iterator @@ -407,7 +421,8 @@ void show_goto_trace( break; case goto_trace_stept::typet::INPUT: - show_state_header(out, step, step.pc->source_location, step.step_nr); + show_state_header( + out, ns, step, step.pc->source_location, step.step_nr, options); out << " INPUT " << step.io_id << ":"; for(std::list::const_iterator @@ -427,7 +442,17 @@ void show_goto_trace( break; case goto_trace_stept::typet::FUNCTION_CALL: + function_depth++; + if(options.show_function_calls) + out << "\n#### Function call: " << step.identifier << " (depth " + << function_depth << ") ####\n"; + break; case goto_trace_stept::typet::FUNCTION_RETURN: + function_depth--; + if(options.show_function_calls) + out << "\n#### Function return: " << step.identifier << " (depth " + << function_depth << ") ####\n"; + break; case goto_trace_stept::typet::SPAWN: case goto_trace_stept::typet::MEMORY_BARRIER: case goto_trace_stept::typet::ATOMIC_BEGIN: diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index 51576939414..43411264ae6 100644 --- a/src/goto-programs/goto_trace.h +++ b/src/goto-programs/goto_trace.h @@ -200,6 +200,8 @@ struct trace_optionst bool json_full_lhs; bool hex_representation; bool base_prefix; + bool show_function_calls; + bool show_code; static const trace_optionst default_options; @@ -208,6 +210,8 @@ struct trace_optionst json_full_lhs = options.get_bool_option("trace-json-extended"); hex_representation = options.get_bool_option("trace-hex"); base_prefix = hex_representation; + show_function_calls = options.get_bool_option("trace-show-function-calls"); + show_code = options.get_bool_option("trace-show-code"); }; private: @@ -216,6 +220,8 @@ struct trace_optionst json_full_lhs = false; hex_representation = false; base_prefix = false; + show_function_calls = false; + show_code = false; }; }; @@ -239,15 +245,23 @@ void trace_value( #define OPT_GOTO_TRACE "(trace-json-extended)" \ + "(trace-show-function-calls)" \ + "(trace-show-code)" \ "(trace-hex)" #define HELP_GOTO_TRACE \ - " --trace-json-extended add rawLhs property to trace\n" \ + " --trace-json-extended add rawLhs property to trace\n" \ + " --trace-show-function-calls show function calls in plain trace\n" \ + " --trace-show-code show original code in plain trace\n" \ " --trace-hex represent plain trace values in hex\n" #define PARSE_OPTIONS_GOTO_TRACE(cmdline, options) \ if(cmdline.isset("trace-json-extended")) \ options.set_option("trace-json-extended", true); \ + if(cmdline.isset("trace-show-function-calls")) \ + options.set_option("trace-show-function-calls", true); \ + if(cmdline.isset("trace-show-code")) \ + options.set_option("trace-show-code", true); \ if(cmdline.isset("trace-hex")) \ options.set_option("trace-hex", true);