From 33acc4e6e97eb084dac201d16665ebf5ac02c081 Mon Sep 17 00:00:00 2001
From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com>
Date: Thu, 8 Oct 2026 10:52:46 +0100
Subject: [PATCH] Skip records in the external-spec pass

Fixes #369. Since the Spoon 11 upgrade, records reach visitCtRecord instead of
visitCtClass, so ExternalRefinementTypeChecker visited a record's methods with
no external target and crashed. It now skips records as it skips classes.
TypeChecker.scan also reports elements without a source file instead of
failing on their position.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 .../src/main/java/testSuite/CorrectRecord.java     | 14 ++++++++++++++
 .../src/main/java/testSuite/ErrorRecordMethod.java | 14 ++++++++++++++
 .../ExternalRefinementTypeChecker.java             |  6 ++++++
 .../processor/refinement_checker/TypeChecker.java  |  4 +++-
 4 files changed, 37 insertions(+), 1 deletion(-)
 create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectRecord.java
 create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorRecordMethod.java

diff --git a/liquidjava-example/src/main/java/testSuite/CorrectRecord.java b/liquidjava-example/src/main/java/testSuite/CorrectRecord.java
new file mode 100644
index 000000000..1a32df906
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/CorrectRecord.java
@@ -0,0 +1,14 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public record CorrectRecord(int x, int y) {
+
+    static int positive(@Refinement("_ > 0") int v) {
+        return v;
+    }
+
+    int sum() {
+        return positive(1) + x + y;
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorRecordMethod.java b/liquidjava-example/src/main/java/testSuite/ErrorRecordMethod.java
new file mode 100644
index 000000000..6d6eab419
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorRecordMethod.java
@@ -0,0 +1,14 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public record ErrorRecordMethod(int x, int y) {
+
+    static int positive(@Refinement("_ > 0") int v) {
+        return v;
+    }
+
+    int bad() {
+        return positive(-1); // Expect: Refinement Error
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java
index a4402c7f2..1339355c0 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java
@@ -17,6 +17,7 @@
 import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtAnnotation;
 import spoon.reflect.declaration.CtClass;
+import spoon.reflect.declaration.CtRecord;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.declaration.CtField;
 import spoon.reflect.declaration.CtInterface;
@@ -39,6 +40,11 @@ public ExternalRefinementTypeChecker(Context context, Factory factory) {
     public <T> void visitCtClass(CtClass<T> ctClass) {
     }
 
+    @Override
+    public void visitCtRecord(CtRecord ctRecord) {
+        // records are user code, like classes: external specs are only read from interfaces
+    }
+
     @Override
     public <T> void visitCtInterface(CtInterface<T> intrface) {
         Optional<CtAnnotation<?>> externalRef = getExternalRefinement(intrface);
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
index 176e33794..ea73e64b9 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
@@ -71,7 +71,9 @@ public void scan(CtElement element) {
             throw e;
         } catch (RuntimeException e) {
             SourcePosition position = element.getPosition();
-            String location = position.getFile().getAbsolutePath() + ":" + position.getLine();
+            String location = position.isValidPosition() && position.getFile() != null
+                    ? position.getFile().getAbsolutePath() + ":" + position.getLine()
+                    : "(no source position: " + element.getClass().getSimpleName() + ")";
             String expression = Utils.getExpressionFromPosition(position);
             String msg = String.format("\nError while checking %s\n  on %s \n  at %s\n  with %s",
                     element.getClass().getSimpleName(), expression, location, e.getMessage());