Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix: Termination override check for certain non-reference trait implementations #5087

Merged
merged 4 commits into from
Feb 14, 2024
Merged

fix: Termination override check for certain non-reference trait implementations #5087

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9ca5216
fix: Termination override check for certain non-reference trait imple…
fabiomadge Feb 14, 2024
0284ce4
add test
fabiomadge Feb 14, 2024
d995e09
format
fabiomadge Feb 14, 2024
66341b7
review
fabiomadge Feb 14, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
add test
  • Loading branch information
@fabiomadge
fabiomadge committed Feb 14, 2024
commit 0284ce4a69710b87271e15f2e7ac3af0d539052f
18 changes: 18 additions & 0 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4982.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
// RUN: %testDafnyForEachResolver "%s" -- --general-traits:datatype

trait Tr {
function Decrease(): nat {
0
}

function F(): nat
decreases Decrease()
}

datatype Dt extends Tr = Dt {
function F(): nat
decreases 0
{
0
}
}
2 changes: 2 additions & 0 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4982.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@

Dafny program verifier finished with 3 verified, 0 errors
Loading