Skip to content

Commit 207110e

Browse files
committed
Add option to show function calls and returns in CBMC trace
1 parent c49ebb7 commit 207110e

File tree

4 files changed

+53
-1
lines changed

4 files changed

+53
-1
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
int function_to_call(int a)
2+
{
3+
int local = 1;
4+
return a+local;
5+
}
6+
7+
8+
int main()
9+
{
10+
int a;
11+
unsigned int b;
12+
a = 0;
13+
a = -100;
14+
a = 2147483647;
15+
b = a*2;
16+
a = -2147483647;
17+
a = function_to_call(a);
18+
b = function_to_call(b);
19+
20+
__CPROVER_assert(0,"");
21+
22+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--trace --trace-show-function-calls
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
Function call: function_to_call \(depth 2\)
7+
Function return: function_to_call \(depth 1\)
8+
Function call: function_to_call \(depth 2\)
9+
10+
^VERIFICATION FAILED$
11+
--
12+
^warning: ignoring

src/goto-programs/goto_trace.cpp

+11
Original file line numberDiff line numberDiff line change
@@ -276,6 +276,7 @@ void show_goto_trace(
276276
{
277277
unsigned prev_step_nr=0;
278278
bool first_step=true;
279+
std::size_t function_depth=0;
279280

280281
for(const auto &step : goto_trace.steps)
281282
{
@@ -420,7 +421,17 @@ void show_goto_trace(
420421
break;
421422

422423
case goto_trace_stept::typet::FUNCTION_CALL:
424+
function_depth++;
425+
if(options.show_function_calls)
426+
out << "\n#### Function call: " << step.identifier << " (depth "
427+
<< function_depth << ") ####\n";
428+
break;
423429
case goto_trace_stept::typet::FUNCTION_RETURN:
430+
function_depth--;
431+
if(options.show_function_calls)
432+
out << "\n#### Function return: " << step.identifier << " (depth "
433+
<< function_depth << ") ####\n";
434+
break;
424435
case goto_trace_stept::typet::SPAWN:
425436
case goto_trace_stept::typet::MEMORY_BARRIER:
426437
case goto_trace_stept::typet::ATOMIC_BEGIN:

src/goto-programs/goto_trace.h

+8-1
Original file line numberDiff line numberDiff line change
@@ -200,6 +200,7 @@ struct trace_optionst
200200
bool json_full_lhs;
201201
bool hex_representation;
202202
bool base_prefix;
203+
bool show_function_calls;
203204

204205
static const trace_optionst default_options;
205206

@@ -208,6 +209,7 @@ struct trace_optionst
208209
json_full_lhs = options.get_bool_option("trace-json-extended");
209210
hex_representation = options.get_bool_option("trace-hex");
210211
base_prefix = hex_representation;
212+
show_function_calls = options.get_bool_option("trace-show-function-calls");
211213
};
212214

213215
private:
@@ -216,6 +218,7 @@ struct trace_optionst
216218
json_full_lhs = false;
217219
hex_representation = false;
218220
base_prefix = false;
221+
show_function_calls = false;
219222
};
220223
};
221224

@@ -239,15 +242,19 @@ void trace_value(
239242

240243

241244
#define OPT_GOTO_TRACE "(trace-json-extended)" \
245+
"(trace-show-function-calls)" \
242246
"(trace-hex)"
243247

244248
#define HELP_GOTO_TRACE \
245-
" --trace-json-extended add rawLhs property to trace\n" \
249+
" --trace-json-extended add rawLhs property to trace\n" \
250+
" --trace-show-function-calls show function calls in plain trace\n" \
246251
" --trace-hex represent plain trace values in hex\n"
247252

248253
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options) \
249254
if(cmdline.isset("trace-json-extended")) \
250255
options.set_option("trace-json-extended", true); \
256+
if(cmdline.isset("trace-show-function-calls")) \
257+
options.set_option("trace-show-function-calls", true); \
251258
if(cmdline.isset("trace-hex")) \
252259
options.set_option("trace-hex", true);
253260

0 commit comments

Comments
 (0)