Fix crash in type checking of nested field assign lhs (#782)

boogie-org · Sep 13, 2023 · c15862c · c15862c
1 parent 074167a
commit c15862c
Show file tree

Hide file tree

Showing 3 changed files with 32 additions and 1 deletion.
diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs
@@ -2362,9 +2362,10 @@ public override void Resolve(ResolutionContext rc)
 
     public override void Typecheck(TypecheckingContext tc)
     {
+      var errorCount = tc.ErrorCount;
       Datatype.Typecheck(tc);
       TypeParameters = SimpleTypeParamInstantiation.EMPTY;
-      if (Datatype.Type != null)
+      if (tc.ErrorCount == errorCount)
       {
         TypeAttr = FieldAccess.Typecheck(Datatype.Type, tc, out TypeParameters);
       }

diff --git a/Test/datatypes/unknown_field_error.bpl b/Test/datatypes/unknown_field_error.bpl
@@ -0,0 +1,27 @@
+// RUN: %parallel-boogie /lib:base "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+type MemAddr;
+type CacheId;
+
+datatype DirState {
+  Owner(i: CacheId),
+  Sharers(i: CacheId)
+}
+
+datatype DirRequest {
+  Share(i: CacheId),
+  Own(i: CacheId)
+}
+
+datatype DirInfo {
+  DirInfo(state: DirState, pending: DirRequest)
+}
+
+var dir: [MemAddr]DirInfo;
+
+procedure cache_snoop_resp(i: CacheId, ma: MemAddr)
+modifies dir;
+{
+  dir[ma]->t->pending := dir[ma]->t->pending;
+}
diff --git a/Test/datatypes/unknown_field_error.bpl.expect b/Test/datatypes/unknown_field_error.bpl.expect
@@ -0,0 +1,3 @@
+unknown_field_error.bpl(26,11): Error: datatype DirInfo does not have a field with name t
+unknown_field_error.bpl(26,34): Error: datatype DirInfo does not have a field with name t
+2 type checking errors detected in unknown_field_error.bpl