From b1cae4452dcaab3931a11f1773677172a60b1870 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 20 Oct 2025 15:54:01 +0100 Subject: [PATCH 1/2] Skip Null Literals in RefinementTypeChecker MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Márcio Caetano <153174341+rodrigomilisse@users.noreply.github.com> --- .../processor/refinement_checker/RefinementTypeChecker.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index b6bfaa12..8cca24a2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -266,6 +266,8 @@ public void visitCtLiteral(CtLiteral lit) { } else if (lit.getType().getQualifiedName().contentEquals("java.lang.String")) { // Only taking care of strings inside refinements + } else if (type == "") { + // Skip null literals for now } else { throw new NotImplementedException( String.format("Literal of type %s not implemented:", lit.getType().getQualifiedName())); From 58789c2fc0b22f542c06b8c434d1eda56e7b1eda Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 21 Oct 2025 08:46:28 +0100 Subject: [PATCH 2/2] Fix String Comparison --- .../refinement_checker/RefinementTypeChecker.java | 8 +++++--- .../src/main/java/liquidjava/utils/Utils.java | 1 + 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 8cca24a2..6d46a535 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -12,6 +12,8 @@ import liquidjava.rj_language.BuiltinFunctionPredicate; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.parsing.ParsingException; +import liquidjava.utils.Utils; + import org.apache.commons.lang3.NotImplementedException; import spoon.reflect.code.CtArrayRead; import spoon.reflect.code.CtArrayWrite; @@ -264,10 +266,10 @@ public void visitCtLiteral(CtLiteral lit) { lit.putMetadata(REFINE_KEY, Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createLit(lit.getValue().toString(), type))); - } else if (lit.getType().getQualifiedName().contentEquals("java.lang.String")) { + } else if (lit.getType().getQualifiedName().equals("java.lang.String")) { // Only taking care of strings inside refinements - } else if (type == "") { - // Skip null literals for now + } else if (type.equals(Utils.NULL_TYPE)) { + // Skip null literals } else { throw new NotImplementedException( String.format("Literal of type %s not implemented:", lit.getType().getQualifiedName())); diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 145707d9..008879cb 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -35,6 +35,7 @@ public class Utils { public static final String SHORT = "short"; public static final String LONG = "long"; public static final String FLOAT = "float"; + public static final String NULL_TYPE = ""; private static final Set DEFAULT_NAMES = Set.of("old", "length", "addToIndex", "getFromIndex");