Add option to show function calls and returns in CBMC trace

Author: polgreen

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,"");
+
+}

regression/cbmc/trace_show_function_calls/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--trace --trace-show-function-calls
+^EXIT=10$
+^SIGNAL=0$
+Function call: function_to_call\(a\)
+Function return
+Function call: function_to_call\(\(signed int\)b\)
+
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/goto-programs/goto_trace.cpp

@@ -420,7 +420,14 @@ void show_goto_trace(
       break;
 
     case goto_trace_stept::typet::FUNCTION_CALL:
+      if(options.show_function_calls)
+        out << "\n####  Function call: " << as_string(ns, *step.pc)
+            << " ####\n";
+      break;
     case goto_trace_stept::typet::FUNCTION_RETURN:
+      if(options.show_function_calls)
+        out << "\n#### Function return ####\n";
+      break;
     case goto_trace_stept::typet::SPAWN:
     case goto_trace_stept::typet::MEMORY_BARRIER:
     case goto_trace_stept::typet::ATOMIC_BEGIN:

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);