[Memory Leak] ESBMC lost track for global managed memory in LinkedList #2335
Description
struct s {
int datum;
struct s *next;
};
struct s *slot[2];
struct s *new(int x) {
struct s *p = malloc(sizeof(struct s));
p->datum = x;
p->next = ((void *)0);
return p;
}
void list_add(struct s *node, struct s *list) {
struct s *temp = list->next;
list->next = node;
node->next = temp;
}
int main () {
slot[0] = new(1);
list_add(new(2), slot[0]);
slot[1] = new(1);
list_add(new(2), slot[1]);
list_add(new(3), slot[1]);
return 0;
}esbmc --no-div-by-zero-check --force-malloc-success --state-hashing --add-symex-value-sets --no-align-check --k-step 2 --floatbv --unlimited-k-steps --no-vla-size-check main.c --memory-leak-check --no-reachable-memory-leak --no-abnormal-memory-leak --malloc-zero-is-null
The counterexample:
[Counterexample]
State 3 file main.c line 1238 column 3 function new thread 0
----------------------------------------------------
p->next = 0
State 10 file main.c line 1243 column 3 function list_add thread 0
----------------------------------------------------
list->next = ( struct s *)((void *)(&dynamic_2_value))
State 14 file main.c line 1238 column 3 function new thread 0
----------------------------------------------------
p->next = 0
State 17 file main.c line 1238 column 3 function new thread 0
----------------------------------------------------
p->next = 0
State 21 file main.c line 1242 column 3 function list_add thread 0
----------------------------------------------------
temp = dynamic_3_value.next
State 25 file main.c line 1243 column 3 function list_add thread 0
----------------------------------------------------
list->next = ( struct s *)((void *)(&dynamic_4_value))
State 27 file main.c line 1244 column 3 function list_add thread 0
----------------------------------------------------
node->next = 0
State 30 file main.c line 1238 column 3 function new thread 0
----------------------------------------------------
p->next = 0
State 34 file main.c line 1242 column 3 function list_add thread 0
----------------------------------------------------
temp = dynamic_3_value.next
State 38 file main.c line 1243 column 3 function list_add thread 0
----------------------------------------------------
list->next = ( struct s *)((void *)(&dynamic_5_value))
State 40 file main.c line 1244 column 3 function list_add thread 0
----------------------------------------------------
node->next = &dynamic_4_value
State 44 file main.c line 1253 column 1 function main thread 0
----------------------------------------------------
Violated property:
file main.c line 1253 column 1 function main
dereference failure: forgotten memory: dynamic_4_value
As all agreed in svcomp, in valid-mem-track, the allocated memory should be freed if it is just managed by local pointers.
The false violation happens at list_add(new(3), slot[1]); when inserting node(3) in the front at slot[1], and when the data structure at slot[1] is node(3) ->node(2)->node(1), esbmc says there is memoy leak for node(2) because it is managed by local pointer (node (3)). However, node(3) is stored at global arr slot, all locally allocated memory can be globally tracked.
In symex_main.cpp we lack a mechanism to identify the maybe_global_target for this case.