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

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
format
  • Loading branch information
@fabiomadge
fabiomadge committed Feb 14, 2024
commit d995e096fbaf9383364e203e98f35c34ac6c100b
4 changes: 2 additions & 2 deletions Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1461,8 +1461,8 @@ private void AddOverrideTerminationChk(ICallable original, ICallable overryd, Bo
// Note, it is as if the trait's method is calling the class's method.
var contextDecreases = overryd.Decreases.Expressions;
var calleeDecreases = original.Decreases.Expressions;
var T = (TraitDecl) (overryd is Function f1 ? f1.EnclosingClass : ((Method)overryd).EnclosingClass);
var I = (TopLevelDeclWithMembers) (original is Function f2 ? f2.EnclosingClass : ((Method)original).EnclosingClass);
var T = (TraitDecl)(overryd is Function f1 ? f1.EnclosingClass : ((Method)overryd).EnclosingClass);
var I = (TopLevelDeclWithMembers)(original is Function f2 ? f2.EnclosingClass : ((Method)original).EnclosingClass);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Instead of the ? :, cast to MemberDecl and then take its .EnclosingClass. Like this:

((MemberDecl)overryd).EnclosingClass

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks I tried for some time, but not hard enough, as it turns out.


// We want to check: calleeDecreases <= contextDecreases (note, we can allow equality, since there is a bounded, namely 1, number of dynamic dispatches)
if (Contract.Exists(contextDecreases, e => e is WildcardExpr)) {
Expand Down
Loading