Built-in function returns hidden in json and xml traces #5207
Description
CBMC version: 5.12 (cbmc-5.12-d8598f8-1368-g5e956891d)
Operating system: MacOS
Exact command line resulting in the issue:
What behaviour did you expect: malloc function return is not hidden
What happened instead: malloc function return is hidden
CBMC traces output by --json-ui and --xml-ui declare the malloc function call to be not hidden and the malloc function return to be hidden. This makes it difficult to ignore internal steps in a trace and still match function calls and returns in a trace representation.
Consider the attached file test.c
#include <stdlib.h>
#include <assert.h>
int main() {
char *x = malloc(1);
assert(0);
}
The command cbmc test.c --json-ui produces output
...
{
"function": {
"displayName": "malloc",
"identifier": "malloc",
"sourceLocation": {
"file": "<builtin-library-malloc>",
"line": "6",
"workingDirectory": "/private/tmp"
}
},
"hidden": false,
"internal": false,
"sourceLocation": {
"file": "test.c",
"function": "main",
"line": "5",
"workingDirectory": "/private/tmp"
},
"stepType": "function-call",
"thread": 0
},
...
{
"function": {
"displayName": "malloc",
"identifier": "malloc",
"sourceLocation": {
"file": "<builtin-library-malloc>",
"line": "6",
"workingDirectory": "/private/tmp"
}
},
"hidden": true,
"internal": false,
"sourceLocation": {
"file": "<builtin-library-malloc>",
"function": "malloc",
"line": "28",
"workingDirectory": "/private/tmp"
},
"stepType": "function-return",
"thread": 0
},
...
The command cbmc test.c --xml-ui produces output
...
<function_call hidden="false" step_nr="24" thread="0">
<function display_name="malloc" identifier="malloc">
<location file="<builtin-library-malloc>" line="6" working-directory="/private/tmp"/>
</function>
<location file="test.c" function="main" line="5" working-directory="/private/tmp"/>
</function_call>
...
<function_return hidden="true" step_nr="42" thread="0">
<function display_name="malloc" identifier="malloc">
<location file="<builtin-library-malloc>" line="6" working-directory="/private/tmp"/>
</function>
<location file="<builtin-library-malloc>" function="malloc" line="28" working-directory="/private/tmp"/>
</function_return>
...