new example and small fixes

Author: CatarinaGamboa

liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/BufferedReaderRefinementsExpert.java

@@ -0,0 +1,58 @@
+package testSuite.classes.ts_bufferedreader_correct;
+import java.io.IOException;
+import java.io.Reader;
+import java.util.stream.Stream;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.RefinementAlias;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@RefinementAlias("NonNegative(int v) { v >= 0 }")
+@RefinementAlias("Positive(int v) { v > 0 }")
+@StateSet({"open", "marked", "closed"})
+@ExternalRefinementsFor("java.io.BufferedReader")
+public interface BufferedReaderRefinementsExpert {
+
+    @StateRefinement(to="open(this)")
+    public void BufferedReader(Reader in);
+
+    @StateRefinement(to="open(this)")
+    public void BufferedReader(Reader in, @Refinement("Positive(_)") int sz);
+
+    @StateRefinement(from="open(this)")
+    @StateRefinement(from="marked(this)")
+    public int read();
+
+    @StateRefinement(from="open(this)")
+    @StateRefinement(from="marked(this)")
+    @Refinement(" _ >= -1")
+    public int read(char[] cbuf, @Refinement("NonNegative(_)") int off, @Refinement("NonNegative(_)") int len);
+
+    @StateRefinement(from="open(this)")
+    @StateRefinement(from="marked(this)")
+    public String readLine() throws IOException;
+
+    @StateRefinement(from="open(this)")
+    @StateRefinement(from="marked(this)")
+    public boolean ready() throws IOException;
+
+    @StateRefinement(from="open(this)")
+    @StateRefinement(from="marked(this)")
+    public boolean markSupported();
+
+    @StateRefinement(from="open(this)", to="marked(this)")
+    @StateRefinement(from="marked(this)")
+    public void mark(@Refinement("NonNegative(_)") int readAheadLimit);
+
+    @StateRefinement(from="marked(this)", to="open(this)")
+    public void reset();
+
+    @StateRefinement(from="!closed(this)", to="closed(this)")
+    public void close();
+
+    @StateRefinement(from="open(this)")
+    @StateRefinement(from="marked(this)")
+    public Stream<String> lines();
+}

liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/Example.java

@@ -0,0 +1,31 @@
+package testSuite.classes.ts_bufferedreader_correct;
+import java.io.BufferedReader;
+import java.io.FileReader;
+import java.io.IOException;
+
+// Regression test for unrefined conditions: each branch reads (open/marked) before
+// closing. The verifier must not assume the if-condition is unconditionally true,
+// otherwise it would conclude the reader is always closed by line 24 and flag the
+// readLine() call on line 31 as a state-refinement error.
+
+class ConfigLoader {
+
+    String loadFirstSetting(String configPath, String defaultValue) throws IOException {
+        BufferedReader reader = new BufferedReader(new FileReader(configPath));
+
+        String header = reader.readLine();
+        if (header.isEmpty()) {
+            reader.close();
+            return defaultValue;
+        }
+
+        if (header.startsWith("#")) {
+            String value = reader.readLine();
+            reader.close();
+            return value;
+        }
+
+        reader.close();
+        return header;
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/BufferedReaderRefinementsExpert.java

@@ -55,4 +55,4 @@ public interface BufferedReaderRefinementsExpert {
     @StateRefinement(from="open(this)")
     @StateRefinement(from="marked(this)")
     public Stream<String> lines();
-}
+}

liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/Example.java

@@ -17,7 +17,7 @@ class ConfigLoader {
 
     String loadFirstSetting(String configPath, String defaultValue) throws IOException {
         BufferedReader reader = new BufferedReader(new FileReader(configPath));
-        
+
         String header = reader.readLine();
         if (header.isEmpty()) {
             reader.close();

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

@@ -25,7 +25,9 @@
 import spoon.reflect.code.CtAssignment;
 import spoon.reflect.code.CtBinaryOperator;
 import spoon.reflect.code.CtBlock;
+import spoon.reflect.code.CtBreak;
 import spoon.reflect.code.CtConditional;
+import spoon.reflect.code.CtContinue;
 import spoon.reflect.code.CtConstructorCall;
 import spoon.reflect.code.CtExpression;
 import spoon.reflect.code.CtFieldRead;
@@ -39,6 +41,7 @@
 import spoon.reflect.code.CtReturn;
 import spoon.reflect.code.CtStatement;
 import spoon.reflect.code.CtThisAccess;
+import spoon.reflect.code.CtThrow;
 import spoon.reflect.code.CtUnaryOperator;
 import spoon.reflect.code.CtVariableAccess;
 import spoon.reflect.code.CtVariableRead;
@@ -399,37 +402,36 @@ public void visitCtIf(CtIf ifElement) {
     }
 
     /**
-     * Returns true when a condition's refinement gives no useful information about which branch may run.
+     * A condition is uninformative when its refinement is the trivial {@code true} predicate yet the expression itself
+     * is not a boolean literal — i.e. the verifier has no symbolic information to relate the branch to. Treating such a
+     * condition as {@code true} would force every if-then to be taken, producing spurious state-refinement errors.
      */
     private boolean isUninformativeCondition(Predicate conditionRefinement, CtExpression<Boolean> condition) {
-        if (!conditionRefinement.isBooleanTrue()) {
+        if (!conditionRefinement.isBooleanTrue())
             return false;
-        }
-        if (condition instanceof CtLiteral<?> literal && literal.getValue() instanceof Boolean) {
-            return false;
-        }
-        return true;
+        return !(condition instanceof CtLiteral<?> literal && literal.getValue() instanceof Boolean);
     }
 
     /**
-     * Best-effort normal-completion check for branch joins. Branches that end in {@code return} cannot contribute state
-     * to the code following the {@code if}.
+     * Best-effort normal-completion check (JLS §14.21): branches that always {@code return} or {@code throw} cannot
+     * contribute state to code following the {@code if}, so their post-context must be discarded at the join.
      */
     private boolean canCompleteNormally(CtStatement statement) {
-        if (statement == null) {
+        if (statement == null)
             return true;
-        }
-        if (statement instanceof CtReturn<?>) {
+        if (statement instanceof CtReturn<?> || statement instanceof CtThrow || statement instanceof CtBreak
+                || statement instanceof CtContinue)
             return false;
-        }
         if (statement instanceof CtBlock<?> block) {
             List<CtStatement> statements = block.getStatements();
             return statements.isEmpty() || canCompleteNormally(statements.get(statements.size() - 1));
         }
         if (statement instanceof CtIf nestedIf) {
             CtStatement elseStatement = nestedIf.getElseStatement();
-            return canCompleteNormally(nestedIf.getThenStatement()) || elseStatement == null
-                    || canCompleteNormally(elseStatement);
+            // No else means the false path always falls through.
+            if (elseStatement == null)
+                return true;
+            return canCompleteNormally(nestedIf.getThenStatement()) || canCompleteNormally(elseStatement);
         }
         return true;
     }