Skip to content
This repository has been archived by the owner on Oct 3, 2021. It is now read-only.

Inconsistency in unreach-call verdicts for verifythis: tree_del_rec.yml, tree_del_iter.yml and tree_max.yml #1237

Open
holznerst opened this issue Nov 24, 2020 · 1 comment

Comments

@holznerst
Copy link
Contributor

There is a inconsistency in the verify this reach-ability category:
There are three benchmark tasks which were split into a safe version and a incorrect version with bug fixes in #851:

In #923 the unreach-call verdicts of the safe tasks were changed to false. We now have a safe version and a incorrect version of each task there both have a false verdict. I don't think this matches the intention of the author, who provided bug fixes for the original tasks.

If I'm right, I would propose to undo the verdict changes and rather fix the tasks if possible.
@gernst could you please have a look, what do you think?

@gernst
Copy link
Contributor

gernst commented Nov 26, 2020

Sorry for my late reply. I recall there was some discussion about these tasks, specifically, that the original version had errors despite the goal of being correct. Hence, I support your proposal, but I don't know really where these bugs were, but memcleanup is of course not valid.
Not sure whether memcleanup should be considered, a recursive free method for trees might cause the unreach-call task to become harder as well, which I would not like.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Development

No branches or pull requests

2 participants