Remove contested LDV tasks #1273
Conversation
|
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. |
|
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). |
|
I was able to confirm memsafety violation for 181 of these benchmarks: #1270 (comment) |
|
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. |
There was a problem hiding this comment.
I am pretty sure that these benchmarks contain undefined behavior (at least most of them: #1270 (comment)), so I'm approving this PR even though there are no fixes for these benchmarks (yet).
I understand the reason why it is good to fix the benchmarks now, but from my point of view, it would not be fair to punish CBMC for mistakes in benchmarks - irrespective of whether we have fixes for them or not.
|
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. |
See #1270.