Treat null literals as carrying no information instead of failing

liquidjava-example/src/main/java/testSuite/CorrectNullLiterals.java

@@ -0,0 +1,54 @@
+package testSuite;
+
+import java.io.ByteArrayOutputStream;
+import java.io.IOException;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class CorrectNullLiterals {
+
+    static void describe(String label, Object value) {
+    }
+
+    public static void main(String[] args) throws IOException {
+        String name = null;
+        if (name == null) {
+            name = "default";
+        }
+        if (name != null) {
+            describe(name, null);
+        }
+
+        ByteArrayOutputStream out = null;
+        try {
+            out = new ByteArrayOutputStream();
+            out.write(1);
+        } finally {
+            if (out != null) {
+                out.close();
+            }
+        }
+
+        // refinements unrelated to the null literals are still checked
+        @Refinement("x > 0")
+        int x = 1;
+        if (name != null) {
+            @Refinement("y > 1")
+            int y = x + 1;
+        }
+    }
+
+    // facts next to a null comparison are kept
+    static void conjunction(String s, int y) {
+        if (s == null && y > 0) {
+            @Refinement("_ > 0")
+            int z = y;
+        }
+    }
+
+    static void ternary(Object o) {
+        @Refinement("_ == -1 || _ == 1")
+        int x = (o == null) ? -1 : 1;
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorNullLiterals.java

@@ -0,0 +1,47 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorNullLiterals {
+
+    // comparisons with null are unknown booleans, so no branch may be considered unreachable
+
+    static void elseBranch(String name) {
+        if (name == null) {
+            System.out.println("none");
+        } else {
+            @Refinement("_ > 0")
+            int x = -1; // Expect: Refinement Error
+        }
+    }
+
+    static void elseBranchOfDisjunction(String name, int y) {
+        if (name == null || y > 0) {
+            System.out.println("some");
+        } else {
+            @Refinement("_ > 0")
+            int x = -1; // Expect: Refinement Error
+        }
+    }
+
+    static void elseBranchOfConjunction(String name, int y) {
+        if (name != null && y > 0) {
+            System.out.println("some");
+        } else {
+            @Refinement("_ <= 0")
+            int z = y; // Expect: Refinement Error
+        }
+    }
+
+    static void ternary(Object o) {
+        @Refinement("_ < 0")
+        int x = (o == null) ? -1 : 1; // Expect: Refinement Error
+    }
+
+    static void booleanValue(Object o) {
+        boolean isNull = o == null;
+        @Refinement("_ == true")
+        boolean b = isNull; // Expect: Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java

@@ -4,7 +4,6 @@
 import java.util.List;
 import java.util.Optional;
 
-import liquidjava.diagnostics.errors.CustomError;
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.processor.context.RefinedFunction;
 import liquidjava.processor.context.RefinedVariable;
@@ -80,6 +79,8 @@ public <T> void getBinaryOpRefinements(CtBinaryOperator<T> operator) throws LJEr
                 && ((CtAssignment<?, ?>) parent).getAssigned()instanceof CtVariableWrite<?> parentVar) {
             oper = getOperationRefinements(operator, parentVar, operator);
 
+        } else if (hasNullOperand(operator)) {
+            oper = createFreshValue(operator, new Predicate()); // null comparisons are not supported yet: unknown value
         } else {
             Predicate varLeft = getOperationRefinements(operator, left);
             Predicate varRight = getOperationRefinements(operator, right);
@@ -224,6 +225,8 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
             rtc.getContext().addVarToContext(elemName, elemVar.getType(), e, elemVar);
             return Predicate.createVar(returnName);
         } else if (element instanceof CtBinaryOperator<?> binop) {
+            if (hasNullOperand(binop)) // null comparisons are not supported yet: unknown boolean value
+                return createFreshValue(binop, new Predicate());
             Predicate right = getOperationRefinements(operator, parentVar, binop.getRightHandOperand());
             Predicate left = getOperationRefinements(operator, parentVar, binop.getLeftHandOperand());
             return Predicate.createOperation(left, getOperatorFromKind(binop.getKind()), right);
@@ -235,12 +238,10 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
             return new Predicate(String.format("(%s)", s), element);
 
         } else if (element instanceof CtLiteral<?> l) {
-            if (l.getType().getQualifiedName().equals("java.lang.String")) {
-                // skip strings
+            if (l.getType().getQualifiedName().equals("java.lang.String") || l.getValue() == null) {
+                // skip strings and null literals (not supported yet, carry no information)
                 return new Predicate();
             }
-            if (l.getValue() == null)
-                throw new CustomError("Null literals are not supported", l.getPosition());
 
             return new Predicate(l.getValue().toString(), element);
 
@@ -299,6 +300,14 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation<?> inv) thr
         return new Predicate();
     }
 
+    private static boolean hasNullOperand(CtBinaryOperator<?> binop) {
+        return isNullLiteral(binop.getLeftHandOperand()) || isNullLiteral(binop.getRightHandOperand());
+    }
+
+    private static boolean isNullLiteral(CtExpression<?> e) {
+        return e instanceof CtLiteral<?> l && l.getValue() == null;
+    }
+
     /**
      * Returns the latest symbolic value for a variable
      */
@@ -327,7 +336,7 @@ private Predicate getOperatorAssignmentRefinement(CtExpression<?> element) throw
             return Predicate.createITE(condition, thenExpression, elseExpression);
         } else if (element instanceof CtLiteral<?> literal) {
             if (literal.getValue() == null)
-                throw new CustomError("Null literals are not supported", literal.getPosition());
+                return new Predicate(); // null literals are not supported yet, carry no information
             return new Predicate(literal.getValue().toString(), element);
         } else if (element instanceof CtInvocation<?>) {
             VariableInstance invocationValue = (VariableInstance) element.getMetadata(Keys.TARGET);