search

sosy-lab / sv-benchmarks

Collection of Verification Tasks (MOVED, please follow the link)
https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
184 stars 169 forks source link

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

Closed tautschnig closed 3 years ago

tautschnig commented 3 years ago

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 commented 3 years ago

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.