Skip to content

Commit

Permalink
fix: Initialize additional fields in the AST (#4930)
Browse files Browse the repository at this point in the history
Fixes #4893
  • Loading branch information
fabiomadge authored Jan 4, 2024
1 parent 4225988 commit 1acddf7
Show file tree
Hide file tree
Showing 4 changed files with 19 additions and 0 deletions.
1 change: 1 addition & 0 deletions Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Ty
Contract.Requires(isRefining ^ (baseType != null));
Contract.Requires(members != null);
BaseType = baseType;
this.NewSelfSynonym();
}
public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, BoundVar bv, Expression constraint,
SubsetTypeDecl.WKind witnessKind, Expression witness, List<Type> parentTraits, List<MemberDecl> members, Attributes attributes, bool isRefining)
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
// RUN: %testDafnyForEachResolver --expect-exit-code=0 "%s"

module A
{
export
provides T

newtype T = int
}

module B
{
import A
type X = A.T
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@

Dafny program verifier finished with 0 verified, 0 errors
1 change: 1 addition & 0 deletions docs/dev/news/4930.fix
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Initialize additional fields in the AST

0 comments on commit 1acddf7

Please sign in to comment.