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

Remove contested LDV tasks #1273

Closed tautschnig closed 3 years ago

tautschnig commented 3 years ago

See #1270.

MartinSpiessl commented 3 years ago

I think this needs more manual inspection to see whether these tasks are really labeled falsely or whether it is a bug in CBMC :thinking:

tautschnig commented 3 years ago

I think this needs more manual inspection to see whether these tasks are really labeled falsely or whether it is a bug in CBMC 🤔

Sure, and I've started doing this with #1274. But I thought I'd rather create this PR first in case some other participants also arrive at result contradicting the claimed verdict and perhaps want to join the effort of debugging these one-by-one.

tautschnig commented 3 years ago

Just to be clear: we are talking about 215 tasks, and I'm simply not too keen for CBMC to be punished when the issue lies in the tasks (or the verdicts).

mchalupa commented 3 years ago

I was able to confirm memsafety violation for 181 of these benchmarks: https://github.com/sosy-lab/sv-benchmarks/issues/1270#issuecomment-743342802

dbeyer commented 3 years ago

We can only remove tasks for which the program was fixed. I think there are some tasks that are removed in this PR for which there is no fix available yet.

tautschnig commented 3 years ago

We can only remove tasks for which the program was fixed. I think there are some tasks that are removed in this PR for which there is no fix available yet.

Yes, 214 left to go. I'll see how many PRs I can manage to create over the remaining ~4 hours. It won't be very many.

dbeyer commented 3 years ago

I understand, and since there is no veto to this PR, I think we can make an exception here and remove those without a fix.