extend plain trace to show function calls and returns

regression/cbmc/hex_trace/main.c

@@ -0,0 +1,12 @@
+int main()
+{
+	int a;
+	unsigned int b;
+	a = 0;
+	a = -100;
+	a = 2147483647;
+	b = a*2;
+	a = -2147483647;
+	__CPROVER_assert(0,"");
+
+}

regression/cbmc/hex_trace/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--trace-hex --trace
+^EXIT=10$
+^SIGNAL=0$
+a=0 \s*\(0x0\)
+b=0ul? \s*\(0x0\)
+a=-100 \s*\(0xFFFFFF9C\)
+a=2147483647 \s*\(0x7FFFFFFF\)
+b=4294967294ul? \s*\(0xFFFFFFFE\)
+a=-2147483647 \s*\(0x80000001\)
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/trace_show_code/main.c

@@ -0,0 +1,23 @@
+int function_to_call(int a)
+{
+	int local = 1;
+	return a+local;
+}
+
+
+int main()
+{
+	int a, c;
+	unsigned int b;
+	a = 0;
+	c = -100;
+	a = function_to_call(a) + function_to_call(c);
+	if(a < 0)
+	  b = function_to_call(b);
+
+	if(c < 0)
+	  b = -function_to_call(b);
+
+	__CPROVER_assert(0,"");
+
+}

regression/cbmc/trace_show_code/test.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+--trace --trace-show-code
+^EXIT=10$
+^SIGNAL=0$
+local = 1
+int a
+int c
+unsigned int b
+a = 0;
+c = -100;
+function_to_call\(a\)
+function_to_call\(c\)
+a = return_value_function_to_call \+ return_value_function_to_call
+function_to_call\(\(signed int\)b\)
+b = \(unsigned int\)return_value_function_to_call
+^VERIFICATION FAILED$
+--
+^warning: ignoring

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,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

src/cbmc/all_properties.cpp

@@ -175,7 +175,8 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
           if(g.second.status==goalt::statust::FAILURE)
           {
             result() << "\n" << "Trace for " << g.first << ":" << "\n";
-            show_goto_trace(result(), bmc.ns, g.second.goto_trace);
+            show_goto_trace(
+              result(), bmc.ns, g.second.goto_trace, bmc.trace_options());
           }
       }
       result() << eom;

src/cbmc/bmc.cpp

@@ -55,7 +55,7 @@ void bmct::error_trace()
   {
   case ui_message_handlert::uit::PLAIN:
     result() << "Counterexample:" << eom;
-    show_goto_trace(result(), ns, goto_trace);
+    show_goto_trace(result(), ns, goto_trace, trace_options());
     result() << eom;
     break;