Skip records in the external-spec pass

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