Double free in termination-recursive-malloc/chunk3.i

[tautschnig]

The task is marked termination:true, but I don't know how to interpret this in presence of undefined behaviour, which is caused by the following lines:

https://github.com/sosy-lab/sv-benchmarks/blob/master/c/termination-recursive-malloc/chunk3.c#L62,L63

These two calls to free amount to a double-free, because the (tail-recursive) procedure chunk sets the two pointers to the same value:

https://github.com/sosy-lab/sv-benchmarks/blob/master/c/termination-recursive-malloc/chunk3.c#L18,L19

There is no case where those two pointers don't have the same value, because chunk will perform at least one recursive call.

[mchalupa]

I can confirm the invalid free in this benchmark.

The task is marked termination:true, but I don't know how to interpret this in presence of undefined behaviour

@tautschnig I think that it was agreed in the past that benchmarks that contain undefined behavior (that is, the benchmark is false(def-behavior) or false(valid-deref) or false(valid-free)), then it should not have any other label than the "undefined" one.