Better `--trace` for `--memory-leak-check`

CBMC version: 5.29.0 Operating system: Mac OS 10.15.7

Testcase:

#include <stdlib.h>

int main() {
  void *p1 = malloc(1), *p2 = malloc(2);
  free(p1);
}

Exact command line resulting in the issue:

cbmc --trace --memory-leak-check test.c | tail -n 21

``` State 86 file /Users/saspadhi/test.c function main line 4 thread 0 ---------------------------------------------------- p2=(const void *)dynamic_object2 (00000011 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 89 file /Users/saspadhi/test.c function main line 5 thread 0 ---------------------------------------------------- ptr=(const void *)dynamic_object1 (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 107 file /Users/saspadhi/test.c function __CPROVER__start line 3 thread 0 ---------------------------------------------------- OUTPUT return': 0 (00000000 00000000 00000000 00000000) Violated property: function __CPROVER__start thread 0 dynamically allocated memory never freed in __CPROVER_memory_leak == NULL __CPROVER_memory_leak == NULL ** 1 of 9 failed (2 iterations) VERIFICATION FAILED ```

What behaviour did you expect: The trace would show the object that was not freed.

What happened instead: The trace just reports that the assertion __CPROVER_memory_leak == NULL failed

Workaround: If I manually track the __CPROVER_memory_leak variable, like:

#include <stdlib.h>

int main() {
  void *p1 = malloc(1), *p2 = malloc(2);
  free(p1);
  void *leaked = __CPROVER_memory_leak;
}

then I see the leaked object in the trace:

cbmc --trace --memory-leak-check new-test.c | tail -n 21

``` State 104 file /Users/saspadhi/new-test.c function main line 6 thread 0 ---------------------------------------------------- leaked=NULL (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 105 file /Users/saspadhi/new-test.c function main line 6 thread 0 ---------------------------------------------------- leaked=(const void *)dynamic_object2 (00000011 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 109 file /Users/saspadhi/new-test.c function __CPROVER__start line 3 thread 0 ---------------------------------------------------- OUTPUT return': 0 (00000000 00000000 00000000 00000000) Violated property: function __CPROVER__start thread 0 dynamically allocated memory never freed in __CPROVER_memory_leak == NULL __CPROVER_memory_leak == NULL ** 1 of 9 failed (2 iterations) VERIFICATION FAILED ```

Would it be possible to automatically insert a variable like this so that the leaked object would be visible in the generated trace?

diffblue / cbmc

Better `--trace` for `--memory-leak-check` #6073