add visit call and examples

Author: CatarinaGamboa

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

@@ -62,4 +62,19 @@ float readAverage(Connection conn) throws SQLException {
             return 0.0f;
         }
     }
+
+    float readAverage2(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().
+        boolean b = parentMessage.next();
+        if( b ) {
+            float avgsum = parentMessage.getFloat("IMPAVG");
+            return avgsum;
+        } else {
+            return 0.0f;
+        }
+    }
 }

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

@@ -67,4 +67,18 @@ float readAverage(Connection conn) throws SQLException {
         float avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error
         return avgsum;
     }
+
+        // Branch-sensitive: 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");
+        float avgsum = 0.0f;
+        boolean b = parentMessage.next();
+        if (b) {
+            avgsum = parentMessage.getFloat("IMPAVG");
+        } else {
+            avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error
+        }
+        return avgsum;
+    }
 }

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

@@ -538,8 +538,10 @@ private Predicate getAssignmentRefinement(String name, CtExpression<?> assignmen
     }
 
     private Predicate getExpressionRefinements(CtExpression<?> element) throws LJError {
-        if (element instanceof CtVariableRead<?>) {
-            // CtVariableRead<?> elemVar = (CtVariableRead<?>) element;
+        if (element instanceof CtFieldRead<?>) {
+            return getRefinement(element);
+        } else if (element instanceof CtVariableRead<?> varRead) {
+            visitCtVariableRead(varRead);
             return getRefinement(element);
         } else if (element instanceof CtBinaryOperator<?>) {
             CtBinaryOperator<?> binop = (CtBinaryOperator<?>) element;