Built-in function returns hidden in json and xml traces

[markrtuttle]

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="&lt;builtin-library-malloc&gt;" 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="&lt;builtin-library-malloc&gt;" line="6" working-directory="/private/tmp"/>
      </function>
      <location file="&lt;builtin-library-malloc&gt;" function="malloc" line="28" working-directory="/private/tmp"/>
    </function_return>
...

[markrtuttle]

test.c.zip

[markrtuttle]

The example still works as described with cbmc 5.37.