bug: functions without body generate incorrect trace

We see a return from main, but wanted to see a return from
function_without_body.

Author: Daniel Kroening

regression/cbmc/trace_show_function_calls/main.c

@@ -4,6 +4,8 @@ int function_to_call(int a)
   return a + local;
 }
 
+int function_without_body(int p);
+
 int main()
 {
   int a;
@@ -15,6 +17,7 @@ int main()
   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