Add option to show function calls and returns in CBMC trace

NathanJPhillips · Jul 6, 2018 · 4fbc10d · 4fbc10d
1 parent f532b4b
commit 4fbc10d
Show file tree

Hide file tree

Showing 4 changed files with 52 additions and 1 deletion.
diff --git a/regression/cbmc/trace_show_function_calls/main.c 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
@@ -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
@@ -283,6 +283,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)
   {
@@ -427,7 +428,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
@@ -200,6 +200,7 @@ struct trace_optionst
   bool json_full_lhs;
   bool hex_representation;
   bool base_prefix;
+  bool show_function_calls;
 
   static const trace_optionst default_options;
 
@@ -208,6 +209,7 @@ 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");
   };
 
 private:
@@ -216,6 +218,7 @@ struct trace_optionst
     json_full_lhs = false;
     hex_representation = false;
     base_prefix = false;
+    show_function_calls = false;
   };
 };
 
@@ -239,15 +242,19 @@ void trace_value(
 
 
 #define OPT_GOTO_TRACE "(trace-json-extended)" \
+                       "(trace-show-function-calls)" \
                        "(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-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-hex"))                                               \
     options.set_option("trace-hex", true);