From 6ac6ff768e44437c4131d2768e477ef9814ca99c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 14 Feb 2026 15:47:38 +0000 Subject: [PATCH 1/2] Fix NullPointerException --- .../MethodsFirstChecker.java | 18 +++++++++++++----- .../MethodsFunctionsChecker.java | 2 ++ 2 files changed, 15 insertions(+), 5 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java index 6a148725..e764d453 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java @@ -96,16 +96,24 @@ public void visitCtInterface(CtInterface intrface) { @Override public void visitCtConstructor(CtConstructor c) { context.enterContext(); - getRefinementFromAnnotation(c); - mfc.getConstructorRefinements(c); - super.visitCtConstructor(c); + try { + getRefinementFromAnnotation(c); + mfc.getConstructorRefinements(c); + super.visitCtConstructor(c); + } catch (LJError e) { + diagnostics.add(e); + } context.exitContext(); } public void visitCtMethod(CtMethod method) { context.enterContext(); - mfc.getMethodRefinements(method); - super.visitCtMethod(method); + try { + mfc.getMethodRefinements(method); + super.visitCtMethod(method); + } catch (LJError e) { + diagnostics.add(e); + } context.exitContext(); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index c2bd580e..68d457f1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -181,6 +181,8 @@ public void getReturnRefinements(CtReturn ret) throws LJError { if (method.getParent() instanceof CtClass) { RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), ((CtClass) method.getParent()).getQualifiedName(), method.getParameters().size()); + if (fi == null) + return; List lv = fi.getArguments(); for (Variable v : lv) { From cb59601c3312d5b36c9f29c2d9c395b316eb6372 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 14 Feb 2026 16:08:50 +0000 Subject: [PATCH 2/2] Add Tests --- .../main/java/testSuite/ErrorInvalidRefinement.java | 13 +++++++++++++ .../testSuite/ErrorInvalidRefinementParameter.java | 13 +++++++++++++ .../testSuite/ErrorInvalidRefinementReturn.java | 11 +++++++++++ .../diagnostics/errors/InvalidRefinementError.java | 2 +- .../general_checkers/MethodsFunctionsChecker.java | 4 ---- 5 files changed, 38 insertions(+), 5 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementParameter.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementReturn.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java new file mode 100644 index 00000000..6933955f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java @@ -0,0 +1,13 @@ +// Invalid Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorInvalidRefinement { + + void test() { + @Refinement("x") + int x = 0; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementParameter.java b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementParameter.java new file mode 100644 index 00000000..c6a92e45 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementParameter.java @@ -0,0 +1,13 @@ +// Invalid Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorInvalidRefinementParameter { + + void testInvalidRefinement(@Refinement("y + 1") int y) {} + + int otherMethod() { + return -1; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementReturn.java b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementReturn.java new file mode 100644 index 00000000..b106518b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementReturn.java @@ -0,0 +1,11 @@ +// Invalid Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorInvalidRefinementReturn { + + @Refinement("_ * 2") + void test() { + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java index cc14bacb..524a422e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java @@ -12,7 +12,7 @@ public class InvalidRefinementError extends LJError { private final String refinement; public InvalidRefinementError(SourcePosition position, String message, String refinement) { - super("Invalid Refinement", message, position, null); + super("Invalid Refinement Error", message, position, null); this.refinement = refinement; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 68d457f1..af16bf92 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -413,10 +413,6 @@ public void loadFunctionInfo(CtExecutable method) { List lv = fi.getArguments(); for (Variable v : lv) rtc.getContext().addVarToContext(v); - } else { - assert false; - // Method should already be in context. Should not arrive this point in - // refinement checker. } } }