Merge pull request diffblue#4265 from diffblue/trace-return-bug

function identifier in trace is wrong when function has no body

Author: tautschnig

regression/cbmc/trace_show_function_calls/main.c

@@ -1,22 +1,23 @@
 int function_to_call(int a)
 {
-	int local = 1;
-	return a+local;
+  int local = 1;
+  return a + local;
 }
 
+int function_without_body(int p);
 
 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,"");
+  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);
+  a = function_without_body(123);
 
+  __CPROVER_assert(0, "");
 }

regression/cbmc/trace_show_function_calls/test.desc

@@ -1,11 +1,13 @@
-CORE broken-smt-backend
+KNOWNBUG broken-smt-backend
 main.c
 --trace --trace-show-function-calls
 ^EXIT=10$
 ^SIGNAL=0$
 Function call: function_to_call\(-2147483647\) \(depth 2\)
 Function return from function_to_call \(depth 1\)
 Function call: function_to_call\(-2\) \(depth 2\)
+Function call: function_without_body\(123\) \(depth 2\)
+Function return from function_without_body \(depth 1\)
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring