Skip records in the external-spec pass (#370)

Fixes #369.

## Problem
Since #363 (Spoon 11), any `record` crashed verification with an NPE in
`TypeChecker.scan`. Spoon 11 dispatches records to `visitCtRecord`;
`ExternalRefinementTypeChecker` overrides only `visitCtClass` (to skip
user classes), so it walked the record's methods with `prefix == null`
and `createReference(null)` threw. Building the error message then
failed on the record's implicit members, which have no source file.

## Change
- `ExternalRefinementTypeChecker.visitCtRecord`: skip, as for classes.
- `TypeChecker.scan`: when the failing element has no source file, the
message says so instead of throwing an NPE.

With this, record methods are verified: a refinement violation inside a
record method is reported (related to #342).

## Tests
- `CorrectRecord`: a record with a method calling a refined method
correctly; crashed on main, now passes.
- `ErrorRecordMethod`: a violation in a record method is reported.
- `mvn test` passes.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

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;
+    }
+}

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
+    }
+}

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);

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());