show function arguments in trace

Author: Daniel Kroening

regression/cbmc/trace_show_function_calls/test.desc

@@ -3,9 +3,9 @@ main.c
 --trace --trace-show-function-calls
 ^EXIT=10$
 ^SIGNAL=0$
-Function call: function_to_call \(depth 2\)
+Function call: function_to_call\(-2147483647\) \(depth 2\)
 Function return: function_to_call \(depth 1\)
-Function call: function_to_call \(depth 2\)
+Function call: function_to_call\(-2\) \(depth 2\)
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

src/goto-programs/goto_trace.cpp

@@ -444,15 +444,34 @@ void show_goto_trace(
     case goto_trace_stept::typet::FUNCTION_CALL:
       function_depth++;
       if(options.show_function_calls)
-        out << "\n#### Function call: " << step.function_identifier
-            << " (depth " << function_depth << ") ####\n";
+      {
+        out << "\n#### Function call: " << step.function_identifier;
+        out << '(';
+
+        bool first = true;
+        for(auto &arg : step.function_arguments)
+        {
+          if(first)
+            first = false;
+          else
+            out << ", ";
+
+          out << from_expr(ns, step.function_identifier, arg);
+        }
+
+        out << ") (depth " << function_depth << ") ####\n";
+      }
       break;
+
     case goto_trace_stept::typet::FUNCTION_RETURN:
       function_depth--;
       if(options.show_function_calls)
+      {
         out << "\n#### Function return: " << step.function_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: