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: Compilation of subset types constrained by type parameter #3893

Merged
merged 15 commits into from
May 4, 2023
Merged

fix: Compilation of subset types constrained by type parameter #3893

Changes from 1 commit
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
162a95e
Add test cases
RustanLeino Apr 20, 2023
d2dca99
fix: Improve Subrange verification to reduce a completeness issue
RustanLeino Apr 20, 2023
1035bed
fix: Crash in resolver
RustanLeino Apr 20, 2023
4bd9803
fix: For Java
RustanLeino Apr 21, 2023
079dde2
fix: For C#
RustanLeino Apr 21, 2023
34a2db0
fix: For Go
RustanLeino Apr 21, 2023
59e1a32
fix: Add cast required by Java for functions
RustanLeino Apr 21, 2023
0b6ecd4
Add tests
RustanLeino Apr 21, 2023
8973cd7
Remove apparently unreachable code
RustanLeino Apr 21, 2023
f65ec61
Update tests
RustanLeino Apr 21, 2023
aa15dc9
Add release notes
RustanLeino Apr 21, 2023
2bd8e7e
Merge branch 'master' into issue-3883
RustanLeino Apr 21, 2023
dc7fb51
Update 3892-fix to cover additional bugs
RustanLeino Apr 22, 2023
539c006
Merge branch 'master' into issue-3883
RustanLeino Apr 26, 2023
d65ad03
Merge branch 'master' into issue-3883
RustanLeino May 4, 2023
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
fix: Improve Subrange verification to reduce a completeness issue 
Fixes #3891
  • Loading branch information
@RustanLeino
RustanLeino committed Apr 21, 2023
commit d2dca994e2827887018d7b80c7359784d2b042e9
11 changes: 8 additions & 3 deletions Source/DafnyCore/Verifier/Translator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7108,7 +7108,7 @@ class BoilerplateTriple { // a triple that is now a quintuple
}
}

public Bpl.Expr CondApplyBox(IToken tok, Bpl.Expr e, Type fromType, Type toType) {
public Bpl.Expr CondApplyBox(Bpl.IToken tok, Bpl.Expr e, Type fromType, Type toType) {
Contract.Requires(tok != null);
Contract.Requires(e != null);
Contract.Requires(fromType != null);
Expand Down Expand Up @@ -7136,7 +7136,7 @@ class BoilerplateTriple { // a triple that is now a quintuple
}
}

public Bpl.Expr BoxIfNecessary(IToken tok, Bpl.Expr e, Type fromType) {
public Bpl.Expr BoxIfNecessary(Bpl.IToken tok, Bpl.Expr e, Type fromType) {
Contract.Requires(tok != null);
Contract.Requires(e != null);
Contract.Requires(fromType != null);
Expand Down Expand Up @@ -9051,8 +9051,13 @@ public ForceCheckToken(IToken tok)
return null;
}
targetType = targetType.NormalizeExpandKeepConstraints();
var cre = MkIs(bSource, targetType);
var udt = targetType as UserDefinedType;
Bpl.Expr cre;
if (udt?.ResolvedClass is RedirectingTypeDecl redirectingTypeDecl && ModeledAsBoxType(redirectingTypeDecl.Var.Type)) {
cre = MkIs(BoxIfNecessary(bSource.tok, bSource, sourceType), TypeToTy(targetType), true);
} else {
cre = MkIs(bSource, targetType);
}
if (udt != null && udt.IsRefType) {
var s = sourceType.NormalizeExpandKeepConstraints();
var certain = false;
Expand Down