diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java index f865a82c9..4e1312265 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java +++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java @@ -62,4 +62,20 @@ float readAverage(Connection conn) throws SQLException { return 0.0f; } } + + float readAverageStoredCondition(Connection conn) throws SQLException { + Statement parentstmt = conn.createStatement(); + ResultSet parentMessage = + parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL"); + // 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"); + return avgsum; + } else { + return 0.0f; + } + } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java index 508b09a82..166c52756 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java +++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java @@ -67,4 +67,29 @@ float readAverage(Connection conn) throws SQLException { float avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error return avgsum; } + + // 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"); + float avgsum = 0.0f; + boolean b = parentMessage.next(); + if (b) { + avgsum = parentMessage.getFloat("IMPAVG"); + } else { + avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error + } + return avgsum; + } } 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 5cc2a09d6..33b5198c8 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 @@ -321,6 +321,10 @@ private boolean tryStaticFinalConstantRefinement(CtFieldRead fieldRead) { public void visitCtVariableRead(CtVariableRead variableRead) { super.visitCtVariableRead(variableRead); CtVariable 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()); } @@ -538,8 +542,11 @@ 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 fieldRead) { + visitCtFieldRead(fieldRead); + return getRefinement(element); + } else if (element instanceof CtVariableRead varRead) { + visitCtVariableRead(varRead); return getRefinement(element); } else if (element instanceof CtBinaryOperator) { CtBinaryOperator binop = (CtBinaryOperator) element;