fix if issue

Author: CatarinaGamboa

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

@@ -0,0 +1,58 @@
+package testSuite.classes.ts_bufferedreader_error;
+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_error/Example.java

@@ -0,0 +1,36 @@
+package testSuite.classes.ts_bufferedreader_error;
+import java.io.BufferedReader;
+import java.io.FileReader;
+import java.io.IOException;
+
+// (A) The model is co-located: BufferedReaderRefinementsExpert (de-packaged
+// copy) declares states open/marked/closed on java.io.BufferedReader and
+// requires open or marked for read methods.
+//
+// (B) The client: load the first non-comment setting from a config file.
+// The author handles three branches — empty file, leading-comment header,
+// plain header — and tries to close the reader as soon as it is no longer
+// needed. In the leading-comment branch the close happens too early; the
+// follow-up readLine runs against a closed reader.
+
+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("#")) {
+            // Header was a comment — the real value is on the next line.
+            reader.close();
+            return reader.readLine(); // State Refinement Error
+        }
+
+        reader.close();
+        return header;
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java

@@ -130,6 +130,8 @@ void saveInstanceElse() {
     Optional<VariableInstance> getIfInstanceCombination(int counter, Predicate cond) {
         if (ifCombiner.isEmpty() || (!has(ifthenIndex) && !has(ifelseIndex) && !has(ifbeforeIndex)))
             return Optional.empty();
+        if (has(ifbeforeIndex) && !has(ifthenIndex) && !has(ifelseIndex))
+            return Optional.empty();
 
         String nName = String.format("#%s_%d", super.getName(), counter);
         Predicate ref = new Predicate();

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

@@ -24,6 +24,7 @@
 import spoon.reflect.code.CtArrayWrite;
 import spoon.reflect.code.CtAssignment;
 import spoon.reflect.code.CtBinaryOperator;
+import spoon.reflect.code.CtBlock;
 import spoon.reflect.code.CtConditional;
 import spoon.reflect.code.CtConstructorCall;
 import spoon.reflect.code.CtExpression;
@@ -36,6 +37,7 @@
 import spoon.reflect.code.CtNewArray;
 import spoon.reflect.code.CtNewClass;
 import spoon.reflect.code.CtReturn;
+import spoon.reflect.code.CtStatement;
 import spoon.reflect.code.CtThisAccess;
 import spoon.reflect.code.CtUnaryOperator;
 import spoon.reflect.code.CtVariableAccess;
@@ -336,18 +338,30 @@ public void visitCtIf(CtIf ifElement) {
         CtExpression<Boolean> exp = ifElement.getCondition();
         Predicate expRefs = getExpressionRefinements(exp);
 
-        String freshVarName = String.format(Formats.FRESH, context.getCounter());
-        expRefs = expRefs.substituteVariable(Keys.WILDCARD, freshVarName);
-        Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs);
-        expRefs = Predicate.createConjunction(expRefs, lastExpRefs);
+        String pathVarName;
+        RefinedVariable freshRV;
+        if (isUninformativeCondition(expRefs, exp)) {
+            // No refinement means the condition is unknown, not true.
+            String conditionVarName = String.format(Formats.FRESH, context.getCounter());
+            context.addInstanceToContext(conditionVarName, factory.Type().BOOLEAN_PRIMITIVE, new Predicate(), exp);
+            expRefs = Predicate.createVar(conditionVarName);
+
+            pathVarName = String.format(Formats.FRESH, context.getCounter());
+            freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, expRefs, exp);
+        } else {
+            pathVarName = String.format(Formats.FRESH, context.getCounter());
+            expRefs = expRefs.substituteVariable(Keys.WILDCARD, pathVarName);
+            Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs);
+            expRefs = Predicate.createConjunction(expRefs, lastExpRefs);
+
+            freshRV = context.addInstanceToContext(pathVarName, factory.Type().INTEGER_PRIMITIVE, expRefs, exp);
+        }
 
         // TODO Change in future
         if (expRefs.getVariableNames().contains("null")) {
             expRefs = new Predicate();
         }
 
-        RefinedVariable freshRV = context.addInstanceToContext(freshVarName, factory.Type().INTEGER_PRIMITIVE, expRefs,
-                exp);
         vcChecker.addPathVariable(freshRV);
 
         context.variablesNewIfCombination();
@@ -357,19 +371,23 @@ public void visitCtIf(CtIf ifElement) {
         // VISIT THEN
         context.enterContext();
         visitCtBlock(ifElement.getThenStatement());
-        context.variablesSetThenIf();
+        if (canCompleteNormally(ifElement.getThenStatement())) {
+            context.variablesSetThenIf();
+        }
         contextHistory.saveContext(ifElement.getThenStatement(), context);
         context.exitContext();
 
         // VISIT ELSE
         if (ifElement.getElseStatement() != null) {
-            context.getVariableByName(freshVarName);
+            context.getVariableByName(pathVarName);
             // expRefs = expRefs.negate();
-            context.newRefinementToVariableInContext(freshVarName, expRefs.negate());
+            context.newRefinementToVariableInContext(pathVarName, expRefs.negate());
 
             context.enterContext();
             visitCtBlock(ifElement.getElseStatement());
-            context.variablesSetElseIf();
+            if (canCompleteNormally(ifElement.getElseStatement())) {
+                context.variablesSetElseIf();
+            }
             contextHistory.saveContext(ifElement.getElseStatement(), context);
             context.exitContext();
         }
@@ -380,6 +398,42 @@ public void visitCtIf(CtIf ifElement) {
         context.variablesFinishIfCombination();
     }
 
+    /**
+     * Returns true when a condition's refinement gives no useful information about which branch may run.
+     */
+    private boolean isUninformativeCondition(Predicate conditionRefinement, CtExpression<Boolean> condition) {
+        if (!conditionRefinement.isBooleanTrue()) {
+            return false;
+        }
+        if (condition instanceof CtLiteral<?> literal && literal.getValue() instanceof Boolean) {
+            return false;
+        }
+        return true;
+    }
+
+    /**
+     * Best-effort normal-completion check for branch joins. Branches that end in {@code return} cannot contribute state
+     * to the code following the {@code if}.
+     */
+    private boolean canCompleteNormally(CtStatement statement) {
+        if (statement == null) {
+            return true;
+        }
+        if (statement instanceof CtReturn<?>) {
+            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);
+        }
+        return true;
+    }
+
     @Override
     public <T> void visitCtArrayWrite(CtArrayWrite<T> arrayWrite) {
         super.visitCtArrayWrite(arrayWrite);