Fixes to parsedAst.cs generation

dafny-lang · Feb 12, 2025 · 816fc76 · 816fc76
1 parent eb80e14
commit 816fc76
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 2 deletions.
diff --git a/Source/DafnyCore/AST/Types/TypeParameterCharacteristics.cs b/Source/DafnyCore/AST/Types/TypeParameterCharacteristics.cs
@@ -16,8 +16,9 @@ public static TypeParameterCharacteristics Default() {
     };
   }
 
-  public TypeParameterCharacteristics(TypeParameter.EqualitySupportValue eqSupport, Type.AutoInitInfo autoInit, bool containsNoReferenceTypes) {
-    EqualitySupport = eqSupport;
+  public TypeParameterCharacteristics(TypeParameter.EqualitySupportValue equalitySupport,
+    Type.AutoInitInfo autoInit, bool containsNoReferenceTypes) {
+    EqualitySupport = equalitySupport;
     AutoInit = autoInit;
     ContainsNoReferenceTypes = containsNoReferenceTypes;
   }

diff --git a/Source/Scripts/ParsedAstGenerator.cs b/Source/Scripts/ParsedAstGenerator.cs
@@ -57,6 +57,14 @@ protected override void HandleClass(Type type) {
         return;
       }
 
+      if (memberInfo.GetCustomAttribute<BackEdge>() != null) {
+        return;
+      }
+
+      if (memberInfo.DeclaringType != type) {
+        return;
+      }
+
       var nullabilityContext = new NullabilityInfoContext();
       var nullabilityInfo = nullabilityContext.Create(parameter);
       bool isNullable = nullabilityInfo.ReadState == NullabilityState.Nullable;

diff --git a/Source/Scripts/PostParseAstVisitor.cs b/Source/Scripts/PostParseAstVisitor.cs
@@ -111,6 +111,10 @@ private void VisitClass(Type type, Stack<Type> toVisit, IDictionary<Type, ISet<T
         return;
       }
 
+      if (field.DeclaringType != type) {
+        return;
+      }
+
       var usedTyped = parameter.ParameterType;
       VisitType(usedTyped, toVisit);
       foreach (var argument in usedTyped.GenericTypeArguments) {