renames and add if null

Author: CatarinaGamboa

liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java

@@ -63,12 +63,13 @@ float readAverage(Connection conn) throws SQLException {
         }
     }
 
-    float readAverage2(Connection conn) throws SQLException {
+    float readAverageStoredCondition(Connection conn) throws SQLException {
         Statement parentstmt = conn.createStatement();
         ResultSet parentMessage =
                 parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL");
-        // FIX (from accepted answer): parentMessage.next();
-        // VIOLATION: cursor is before the first row; getFloat() with no next().
+        // Regression for issue #241: next()'s result is stored in a boolean before the `if`.
+        // The transition (_ ? onRow : endRows) must still flow through `b`, so the guarded
+        // getFloat() is on a row (onRow) and verifies — exactly as the inline readAverage above.
         boolean b = parentMessage.next();
         if( b ) {
             float avgsum = parentMessage.getFloat("IMPAVG");

liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java

@@ -68,7 +68,18 @@ float readAverage(Connection conn) throws SQLException {
         return avgsum;
     }
 
-        // Branch-sensitive: legal in the then-branch (onRow), illegal in the else-branch (endRows).
+    // Issue #241 soundness: storing next()'s result in a boolean must NOT make getFloat()
+    // unconditionally legal. With no guard the state is `next ? onRow : endRows`, so onRow is
+    // not guaranteed and getFloat() must still be rejected.
+    float readAverageStoredNoGuard(Connection conn) throws SQLException {
+        Statement parentstmt = conn.createStatement();
+        ResultSet parentMessage = parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL");
+        boolean b = parentMessage.next();
+        float avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error
+        return avgsum;
+    }
+
+    // Issue #241 branch-sensitivity: legal in the then-branch (onRow), illegal in the else-branch (endRows).
     float readAverageVarElse(Connection conn) throws SQLException {
         Statement parentstmt = conn.createStatement();
         ResultSet parentMessage = parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL");

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

@@ -321,6 +321,10 @@ private <T> boolean tryStaticFinalConstantRefinement(CtFieldRead<T> fieldRead) {
     public <T> void visitCtVariableRead(CtVariableRead<T> variableRead) {
         super.visitCtVariableRead(variableRead);
         CtVariable<T> varDecl = variableRead.getVariable().getDeclaration();
+        // Some CtVariableRead forms have no resolvable declaration (e.g. accesses to symbols outside the
+        // model); with no name there is no context entry to attach, so leave the metadata as-is.
+        if (varDecl == null)
+            return;
         getPutVariableMetadata(variableRead, varDecl.getSimpleName());
     }
 
@@ -539,8 +543,15 @@ private Predicate getAssignmentRefinement(String name, CtExpression<?> assignmen
 
     private Predicate getExpressionRefinements(CtExpression<?> element) throws LJError {
         if (element instanceof CtFieldRead<?>) {
+            // CtFieldRead is a subtype of CtVariableRead and MUST be matched first: field reads (including
+            // the array pseudo-field `.length`, whose declaration is null) are handled by visitCtFieldRead
+            // during the surrounding scan, so here we just read the metadata it already set.
             return getRefinement(element);
         } else if (element instanceof CtVariableRead<?> varRead) {
+            // Visit the read so its metadata becomes `_ == <last instance>`, linking the variable to the
+            // instance that carries its refinement (e.g. a stored method result). Without this, `if (b)`
+            // looks refinement-free and is treated as uninformative, dropping the typestate that b's
+            // defining call established (#241).
             visitCtVariableRead(varRead);
             return getRefinement(element);
         } else if (element instanceof CtBinaryOperator<?>) {