diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index e0bda007c..764e1165c 100644 --- 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 new file mode 100644 index 000000000..318bb5c72 --- /dev/null +++ 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 new file mode 100644 index 000000000..6c4caadff --- /dev/null +++ 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