From 850ffbfdcd88f7d6be666ce43d46a25565631aa6 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 20 Jul 2026 22:21:59 +0100 Subject: [PATCH 1/2] Release liquidjava-verifier 0.0.28 --- liquidjava-verifier/pom.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index cbb415ce..84499855 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -11,7 +11,7 @@ io.github.liquid-java liquidjava-verifier - 0.0.27 + 0.0.28 liquidjava-verifier LiquidJava Verifier https://github.com/liquid-java/liquidjava From e5a6eb558d082b8c9e70724a2e8b051af299e03c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 27 Jul 2026 14:34:44 +0100 Subject: [PATCH 2/2] Fix Inconsistent Qualified Names --- .../conflicting_ghost_names_correct/SimpleTest.java | 6 ++++-- .../conflicting_ghost_names_correct/StackRefinements.java | 4 ++++ .../processor/refinement_checker/TypeChecker.java | 4 +++- .../liquidjava/rj_language/ast/FunctionInvocation.java | 7 ++----- 4 files changed, 13 insertions(+), 8 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/SimpleTest.java index 99f525bb..8f98d10d 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/SimpleTest.java +++ b/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/SimpleTest.java @@ -10,8 +10,10 @@ public void example() { list.get(0); Stack stack = new Stack<>(); - stack.push(1); - stack.peek(); + if (stack.empty()) { + stack.push(1); + stack.peek(); + } stack.pop(); } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/StackRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/StackRefinements.java index f94b5d02..ffe361d2 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/StackRefinements.java +++ b/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/StackRefinements.java @@ -2,6 +2,7 @@ import liquidjava.specification.ExternalRefinementsFor; import liquidjava.specification.Ghost; +import liquidjava.specification.Refinement; import liquidjava.specification.StateRefinement; @ExternalRefinementsFor("java.util.Stack") @@ -18,4 +19,7 @@ public interface StackRefinements { @StateRefinement(from="size(this) > 0") public E peek(); + + @Refinement("_ ? size(this) == 0 : size(this) > 0") + public boolean empty(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 4935b457..36c4e0ea 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -105,7 +105,9 @@ public Optional getRefinementFromAnnotation(CtElement element) throws } } if (ref.isPresent()) { - Predicate p = new Predicate(ref.get(), element); + String prefix = getQualifiedClassName(element); + Predicate p = prefix == null ? new Predicate(ref.get(), element) + : new Predicate(ref.get(), element, prefix); if (!p.getExpression().isBooleanExpression()) { SourcePosition position = Utils.getLJAnnotationPosition(element, ref.get()); throw new InvalidRefinementError(position, "Refinement predicate must be a boolean expression", diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java index 85af21b4..d9d53731 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java @@ -93,7 +93,7 @@ public int hashCode() { final int prime = 31; int result = 1; result = prime * result + ((getArgs() == null) ? 0 : getArgs().hashCode()); - result = prime * result + ((name == null) ? 0 : Utils.getSimpleName(name).hashCode()); // same here + result = prime * result + ((name == null) ? 0 : name.hashCode()); return result; } @@ -114,10 +114,7 @@ public boolean equals(Object obj) { if (name == null) { return other.name == null; } else { - // prefixes are inconsistent for refined class ghost calls: some use the - // original class prefix, others use the caller class prefix - // for now we compare simple names, but prefix handling should be fixed instead of having this workaround - return other.name != null && Utils.getSimpleName(name).equals(Utils.getSimpleName(other.name)); + return name.equals(other.name); } } }