Merge branch 'master' into highprecision

nickbattle · Dec 3, 2023 · 4898562 · 4898562
2 parents 79daa1f + 4693a35
commit 4898562
Showing 1 changed file with 11 additions and 0 deletions.
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/patterns/TCRecordPattern.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/patterns/TCRecordPattern.java
@@ -26,6 +26,7 @@
 
 import com.fujitsu.vdmj.tc.lex.TCNameToken;
 import com.fujitsu.vdmj.tc.patterns.visitors.TCPatternVisitor;
+import com.fujitsu.vdmj.tc.types.TCRecordType;
 import com.fujitsu.vdmj.tc.types.TCType;
 import com.fujitsu.vdmj.tc.types.TCUnresolvedType;
 import com.fujitsu.vdmj.typechecker.Environment;
@@ -92,6 +93,16 @@ public void typeResolve(Environment env)
 		{
 			plist.typeResolve(env);
 			type = type.typeResolve(env);
+
+			if (type instanceof TCRecordType)
+			{
+				TCRecordType recordType = (TCRecordType)type;
+
+				if (recordType.opaque && !location.module.equals(recordType.location.module))
+				{
+					report(3127, "Type '" + typename + "' has no struct export");
+				}
+			}
 		}
 		catch (TypeCheckException e)
 		{