From e8bb37ce8111cbb87fff264e0a788f65fac1fb7a Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 12:30:56 +0000 Subject: [PATCH 1/2] Treat an argument with no known refinement as unconstrained An argument whose refinement is just `true` (e.g. the result of a method without refinements) was turned into `arg == true`. For an int argument that crashed with "Sorts Int and Bool are incompatible"; for a boolean one it wrongly assumed the value was true. Fixes #451 Co-Authored-By: Claude Opus 5.5 --- .../testSuite/ErrorUnknownMethodInOperation.java | 13 +++++++++++++ .../general_checkers/MethodsFunctionsChecker.java | 4 +++- 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInOperation.java b/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInOperation.java index 177dab743..3ca462a43 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInOperation.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnknownMethodInOperation.java @@ -9,4 +9,17 @@ public void lengthPlusOne(String s) { @Refinement("_ > 0") int x = s.length() + 1; // Expect: Refinement Error } + + static void take(@Refinement("_ > 0") int amount) {} + + static void takeTrue(@Refinement("_ == true") boolean flag) {} + + // also when passed straight as an argument (issue #451) + public void lengthAsArgument(String s) { + take(s.length()); // Expect: Refinement Error + } + + public void isEmptyAsArgument(String s) { + takeTrue(s.isEmpty()); // Expect: Refinement Error + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 8c8f4ade3..0bf473e69 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -456,7 +456,9 @@ private String createVariableRepresentingArgument(CtExpression iArg, Variable Predicate met = (Predicate) iArg.getMetadata(Keys.REFINEMENT); if (met == null) met = new Predicate(); - if (!met.getVariableNames().contains(Keys.WILDCARD)) + // `true` means nothing is known about the argument (e.g. the result of an unrefined call), not that it equals + // true + if (!met.isBooleanTrue() && !met.getVariableNames().contains(Keys.WILDCARD)) met = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), met); String nVar = String.format(Formats.INSTANCE, fArg.getName(), rtc.getContext().getCounter()); rtc.getContext().addInstanceToContext(nVar, fArg.getType(), met.substituteVariable(Keys.WILDCARD, nVar), iArg); From 54a6de79915420ed06493cdf0bc9b666b15cad4b Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 12:43:56 +0000 Subject: [PATCH 2/2] Skip the equality only for a bare true, not a true-valued expression Co-Authored-By: Claude Opus 5.5 --- .../general_checkers/MethodsFunctionsChecker.java | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 0bf473e69..0e21f2fbf 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -16,6 +16,7 @@ import liquidjava.processor.refinement_checker.object_checkers.AuxHierarchyRefinementsPassage; import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.formatter.ArgumentDisplayNames; import liquidjava.utils.GeneratedNames; import liquidjava.utils.Utils; @@ -456,9 +457,10 @@ private String createVariableRepresentingArgument(CtExpression iArg, Variable Predicate met = (Predicate) iArg.getMetadata(Keys.REFINEMENT); if (met == null) met = new Predicate(); - // `true` means nothing is known about the argument (e.g. the result of an unrefined call), not that it equals - // true - if (!met.isBooleanTrue() && !met.getVariableNames().contains(Keys.WILDCARD)) + // a bare `true` means nothing is known about the argument (e.g. the result of an unrefined call), not that it + // equals true + boolean unknown = met.getExpression()instanceof LiteralBoolean b && b.isBooleanTrue(); + if (!unknown && !met.getVariableNames().contains(Keys.WILDCARD)) met = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), met); String nVar = String.format(Formats.INSTANCE, fArg.getName(), rtc.getContext().getCounter()); rtc.getContext().addInstanceToContext(nVar, fArg.getType(), met.substituteVariable(Keys.WILDCARD, nVar), iArg);