From 46cd46c3a901614e79e89257330869fd817bd6e0 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 6 May 2026 16:50:54 +0100 Subject: [PATCH 1/6] fix if issue --- .../BufferedReaderRefinementsExpert.java | 58 +++++++++++++++ .../ts_bufferedreader_error/Example.java | 36 +++++++++ .../processor/context/Variable.java | 2 + .../RefinementTypeChecker.java | 74 ++++++++++++++++--- 4 files changed, 160 insertions(+), 10 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/BufferedReaderRefinementsExpert.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/Example.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/BufferedReaderRefinementsExpert.java b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/BufferedReaderRefinementsExpert.java new file mode 100644 index 00000000..485c4612 --- /dev/null +++ b/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 lines(); +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/Example.java b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/Example.java new file mode 100644 index 00000000..aeb3b183 --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java index 8ea8f67e..cfed765d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java @@ -130,6 +130,8 @@ void saveInstanceElse() { Optional 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(); 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 c1dace74..f631de15 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 @@ -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 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 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 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 void visitCtArrayWrite(CtArrayWrite arrayWrite) { super.visitCtArrayWrite(arrayWrite); From 70f3f083982ba884a4af2732bb88847ddc8b40a2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 6 May 2026 20:13:05 +0100 Subject: [PATCH 2/6] new example and small fixes --- .../BufferedReaderRefinementsExpert.java | 58 +++++++++++++++++++ .../ts_bufferedreader_correct/Example.java | 31 ++++++++++ .../BufferedReaderRefinementsExpert.java | 2 +- .../ts_bufferedreader_error/Example.java | 2 +- .../RefinementTypeChecker.java | 32 +++++----- 5 files changed, 108 insertions(+), 17 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/BufferedReaderRefinementsExpert.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/Example.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/BufferedReaderRefinementsExpert.java b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/BufferedReaderRefinementsExpert.java new file mode 100644 index 00000000..6a437f45 --- /dev/null +++ b/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 lines(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/Example.java b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/Example.java new file mode 100644 index 00000000..eb8e1a74 --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/BufferedReaderRefinementsExpert.java b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/BufferedReaderRefinementsExpert.java index 485c4612..a6e87a44 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/BufferedReaderRefinementsExpert.java +++ b/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 lines(); -} \ No newline at end of file +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/Example.java b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/Example.java index aeb3b183..7ffe5e53 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/Example.java +++ b/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(); 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 f631de15..edd53777 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 @@ -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 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 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; } From 3f3e46931edaa3ada6e4757f02438bd36410304a Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Thu, 7 May 2026 13:24:19 +0100 Subject: [PATCH 3/6] simplify needed vars --- .../RefinementTypeChecker.java | 26 +++++++++---------- 1 file changed, 13 insertions(+), 13 deletions(-) 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 edd53777..50ba05f5 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 @@ -341,18 +341,14 @@ public void visitCtIf(CtIf ifElement) { CtExpression exp = ifElement.getCondition(); Predicate expRefs = getExpressionRefinements(exp); - String pathVarName; + String pathVarName = String.format(Formats.FRESH, context.getCounter()); 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); + // No refinement means the condition is unknown, not true: model it as a fresh + // boolean so the SMT solver may pick either truth value for each branch. + expRefs = Predicate.createVar(pathVarName); + freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, new Predicate(), exp); } else { - pathVarName = String.format(Formats.FRESH, context.getCounter()); expRefs = expRefs.substituteVariable(Keys.WILDCARD, pathVarName); Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs); expRefs = Predicate.createConjunction(expRefs, lastExpRefs); @@ -382,8 +378,6 @@ public void visitCtIf(CtIf ifElement) { // VISIT ELSE if (ifElement.getElseStatement() != null) { - context.getVariableByName(pathVarName); - // expRefs = expRefs.negate(); context.newRefinementToVariableInContext(pathVarName, expRefs.negate()); context.enterContext(); @@ -413,8 +407,14 @@ private boolean isUninformativeCondition(Predicate conditionRefinement, CtExpres } /** - * 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. + * Best-effort normal-completion check (JLS §14.21): branches that always {@code return}, {@code throw}, + * {@code break} or {@code continue} cannot contribute state to code following the {@code if}, so their post-context + * must be discarded at the join. + * + *

+ * Not currently handled (treated conservatively as completing normally): {@code switch} where every case exits, + * labeled {@code break}/{@code continue} targets, {@code try}/{@code catch}/{@code finally} flow, and infinite + * loops such as {@code while (true)}. Extending this list only tightens precision. */ private boolean canCompleteNormally(CtStatement statement) { if (statement == null) From b3c19e94cee68ac5c151df5c5ed7cf4d650651fd Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Thu, 7 May 2026 13:31:16 +0100 Subject: [PATCH 4/6] added minor example --- .../src/main/java/testSuite/CorrectIfThen.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/liquidjava-example/src/main/java/testSuite/CorrectIfThen.java b/liquidjava-example/src/main/java/testSuite/CorrectIfThen.java index c7fa9119..9e5ed044 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectIfThen.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectIfThen.java @@ -25,6 +25,14 @@ public void have1(int a) { int u = pos; } + public void haveAnd(int a, @Refinement("b > 5")int b) { + @Refinement("pos > 0") + int pos = 10; + if (a > 0 && b > 0) { + if (a > b) pos = a - b; + } + } + public static void main(String[] args) { @Refinement("_ < 10") int a = 5; From a7608dcdafe2dca57828871fcd31b500d632cb46 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 8 May 2026 11:56:25 +0100 Subject: [PATCH 5/6] example of no return with error --- .../classes/ts_bufferedreader_error/Example.java | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/Example.java b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/Example.java index 7ffe5e53..bc3f1810 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/Example.java +++ b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/Example.java @@ -33,4 +33,16 @@ String loadFirstSetting(String configPath, String defaultValue) throws IOExcepti reader.close(); return header; } + + String loadFirstSetting2(String configPath, String defaultValue) throws IOException { + BufferedReader reader = new BufferedReader(new FileReader(configPath)); + + String header = reader.readLine(); + if (header.isEmpty()) { + reader.close(); + // no return here + } + reader.close(); // State Refinement Error + return header; + } } From ecd496f84cb0accc00d433c7250068e369581201 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 8 May 2026 12:02:19 +0100 Subject: [PATCH 6/6] update filenames --- .../ts_bufferedreader_correct/{Example.java => ConfigLoader.java} | 0 .../ts_bufferedreader_error/{Example.java => ConfigLoader.java} | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/{Example.java => ConfigLoader.java} (100%) rename liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/{Example.java => ConfigLoader.java} (100%) diff --git a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/Example.java b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/ConfigLoader.java similarity index 100% rename from liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/Example.java rename to liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/ConfigLoader.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/Example.java b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/ConfigLoader.java similarity index 100% rename from liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/Example.java rename to liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/ConfigLoader.java