Remove Fields Implicit Null Refinement

liquid-java · rcosta358 · Feb 7, 2026 · Feb 7, 2026 · Feb 7, 2026 · Feb 8, 2026
commit c739e5f096fb4f3ae185dd2af2d0ba9c85d26f16
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNullCheckFieldAssignment.java b/liquidjava-example/src/main/java/testSuite/ErrorNullCheckFieldAssignment.java
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNullCheckFieldNonInitialized.java b/liquidjava-example/src/main/java/testSuite/ErrorNullCheckFieldNonInitialized.java
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNullableFieldNonNullAssumption.java b/liquidjava-example/src/main/java/testSuite/ErrorNullableFieldNonNullAssumption.java
@@ -0,0 +1,14 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorNullableFieldNonNullAssumption {
+    Integer x;
+
+    void test() {
+        mustBeNonNull(x); // we dont know if x is null or not
+    }
+
+    void mustBeNonNull(@Refinement("_ != null") Integer i) {}
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNullableFieldNullAssumption.java b/liquidjava-example/src/main/java/testSuite/ErrorNullableFieldNullAssumption.java
@@ -0,0 +1,14 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorNullableFieldNullAssumption {
+    Integer x;
+
+    void test() {
+        mustBeNull(x); // we dont know if x is null or not
+    }
+
+    void mustBeNull(@Refinement("_ == null") Integer i) {}
+}
diff --git a/...verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/...verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
@@ -246,14 +246,6 @@ public <T> void visitCtField(CtField<T> f) {
         if (v instanceof Variable) {
             ((Variable) v).setLocation("this");
         }
-        // if the field is not initialized and can be null, add instance to context with null equality refinement
-        if (f.getAssignment() == null && !Utils.isPrimitiveType(f.getType().getQualifiedName())) {
-            String instanceName = String.format(Formats.INSTANCE, name, context.getCounter());
-            Predicate initialRefinement = Predicate.createConjunction(ret.substituteVariable(name, instanceName),
-                    Predicate.createNullEq().substituteVariable(Keys.WILDCARD, instanceName));
-            context.addInstanceToContext(instanceName, f.getType(), initialRefinement, f);
-            context.addRefinementInstanceToVariable(name, instanceName);
-        }
     }
 
     @Override
@@ -270,13 +262,9 @@ public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
             }
 
         } else if (context.hasVariable(String.format(Formats.THIS, fieldName))) {
-            // resolve to latest instance of this field for flow-sensitive refinement
             String thisName = String.format(Formats.THIS, fieldName);
-            Optional<VariableInstance> ovi = context.getLastVariableInstance(thisName);
-            String var = ovi.isPresent() ? ovi.get().getName() : thisName;
             fieldRead.putMetadata(Keys.REFINEMENT,
-                    Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(var)));
-
+                    Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName)));
         } else if (fieldRead.getVariable().getSimpleName().equals("length")) {
             String targetName = fieldRead.getTarget().toString();
             fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD),