Include property information in json output

[zhassan-aws]

CBMC version: 5.48.0
Operating system: Ubuntu 20.04.2

This is a feature request. Currently, CBMC's json output (--json-ui) does not include some of the information on the properties (file, line, and function). For example, for:

#include "assert.h"

void foo(int x, int y) {
  assert(x == y);
}

void bar(int x, int y) {
  assert(x != y);
}

int main() {
  foo(5, 5);
  bar(3, 7);
  return 0;
}

The "result" section of the json output is as follows:

$ cbmc multi.c --json-ui
.
.
.
    "result": [
      {
        "description": "assertion x == y",
        "property": "foo.assertion.1",
        "status": "SUCCESS"
      },
      {
        "description": "assertion x != y",
        "property": "bar.assertion.1",
        "status": "SUCCESS"
      }
    ]
  },

and the property information is not included anywhere in the json. The only way to get the property information is to rerun CBMC with --show-properties. This requires merging the json output from the two CBMC runs though.

Since the non-json output includes the property information:

$ cbmc multi.c 
CBMC version 5.48.0 (cbmc-5.48.0) 64-bit x86_64 linux
.
.
.

** Results:
multi.c function bar
[bar.assertion.1] line 8 assertion x != y: SUCCESS

multi.c function foo
[foo.assertion.1] line 4 assertion x == y: SUCCESS

** 0 of 2 failed (1 iterations)
VERIFICATION SUCCESSFUL

would it be possible to include it in the json output as well?