This repository has been archived by the owner on Oct 3, 2021. It is now read-only.
fix labels of two termination benchmarks #292
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
- Addition02_false-unreach-call_true-termination.c for n > 0 termination can be shown using the ranking function f(m, n)=n for n < 0 termination can be shown using the ranking function f(m, n)=-n - McCarthy91_false-unreach-call_true-termination.c Our tool does not provide a simple termination proof, however it is well-known that this algorithm is terminating and the implementation does not contain any "surprises" like e.g. operations with wrap-around arithmetic
label of EvenOdd03 was already incorrect before my overflow fixes
(avoid that the large number of termination benchmarks in product-lines outweigts other termination benchmarks)
(avoid that the large number of termination benchmarks in product-lines outweigts other termination benchmarks)
… also recursive-simple to Termination-Recursive.set
PhilippWendler
suggested changes
Dec 3, 2016
There was a problem hiding this comment.
Could you please split this PR into at least two: changing existing files in one PR, and adding termination labels to files in another? This would make it easier to review and discuss the changes.
When you rename files, please check whether they are listed in the blacklist in compare.sh and update their names there as well to prevent failure of the continuous integration check.
Also, please run check.py and fix any reported errors. Thanks!
This was referenced Dec 3, 2016
Closed
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Addition02_false-unreach-call_true-termination.c
for n > 0 termination can be shown using the ranking function f(m, n)=n
for n < 0 termination can be shown using the ranking function f(m, n)=-n
McCarthy91_false-unreach-call_true-termination.c
Our tool does not provide a simple termination proof, however it is
well-known that this algorithm is terminating and the implementation
does not contain any "surprises" like e.g. operations with wrap-around arithmetic