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..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,8 +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.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");