Open
Description
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?