From 4fbc10da0f82eef780eb906781362611e3e11400 Mon Sep 17 00:00:00 2001
From: Polgreen <polgreen@amazon.com>
Date: Tue, 3 Jul 2018 13:39:00 +0200
Subject: [PATCH] Add option to show function calls  and returns in CBMC trace

---
 .../cbmc/trace_show_function_calls/main.c     | 22 +++++++++++++++++++
 .../cbmc/trace_show_function_calls/test.desc  | 11 ++++++++++
 src/goto-programs/goto_trace.cpp              | 11 ++++++++++
 src/goto-programs/goto_trace.h                |  9 +++++++-
 4 files changed, 52 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/trace_show_function_calls/main.c
 create mode 100644 regression/cbmc/trace_show_function_calls/test.desc

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..86e4429715a 100644
--- 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
index 51576939414..295905d2b46 100644
--- 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);