From 71bd869871b36bad45fb3c717b463f243f8fcdcf Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 3 Nov 2025 16:03:49 +0000 Subject: [PATCH] Fix Ghost Qualified Names --- .../ArrayListRefinements.java | 18 ++++++++++++++++ .../SimpleTest.java | 17 +++++++++++++++ .../StackRefinements.java | 21 +++++++++++++++++++ .../object_checkers/AuxStateHandler.java | 2 +- 4 files changed, 57 insertions(+), 1 deletion(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/ArrayListRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/SimpleTest.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/StackRefinements.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/ArrayListRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/ArrayListRefinements.java new file mode 100644 index 00000000..c1c9151a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/ArrayListRefinements.java @@ -0,0 +1,18 @@ +package testSuite.classes.conflicting_ghost_names_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Ghost; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; + +@ExternalRefinementsFor("java.util.ArrayList") +@Ghost("int size") +public interface ArrayListRefinements { + + public void ArrayList(); + + @StateRefinement(to = "size(this) == (size(old(this)) + 1)") + public boolean add(E elem); + + public E get(@Refinement("0 <= _ && _ < size(this)") int index); +} 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 new file mode 100644 index 00000000..99f525bb --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/SimpleTest.java @@ -0,0 +1,17 @@ +package testSuite.classes.conflicting_ghost_names_correct; + +import java.util.ArrayList; +import java.util.Stack; + +public class SimpleTest { + public void example() { + ArrayList list = new ArrayList<>(); + list.add(10); + list.get(0); + + Stack stack = new Stack<>(); + 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 new file mode 100644 index 00000000..155d844b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/StackRefinements.java @@ -0,0 +1,21 @@ +package testSuite.classes.conflicting_ghost_names_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; + +@ExternalRefinementsFor("java.util.Stack") +@Ghost("int size") +public interface StackRefinements { + + public void Stack(); + + @StateRefinement(to="size(this) == size(old(this)) + 1") + public boolean push(E elem); + + @StateRefinement(from="size(this) > 0", to="size(this) == size(old(this)) - 1") + public E pop(); + + @StateRefinement(from="size(this) > 0") + public E peek(); +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 72ada2df..99f13890 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -84,7 +84,7 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) { case "double" -> Predicate.createLit("0.0", Utils.DOUBLE); default -> throw new RuntimeException("Ghost not implemented for type " + retType); }; - Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s), typePredicate); + Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getQualifiedName(), s), typePredicate); c = Predicate.createConjunction(c, p); } ObjectState os = new ObjectState();