Skip to content

Built-in function returns hidden in json and xml traces #5207

Open
@markrtuttle

Description

@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>
...

Metadata

Metadata

Assignees

No one assigned

    Labels

    ViewerBugs and features related to CBMC ViewerawsBugs or features of importance to AWS CBMC usersbug

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions