Fix Ghost Qualified Names

Author: rcosta358

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<E> {
+
+	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);
+}

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<Integer> list = new ArrayList<>();
+        list.add(10);
+        list.get(0);
+
+        Stack<Integer> stack = new Stack<>();
+		stack.push(1);
+		stack.peek();
+		stack.pop();
+    }
+}

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<E> {
+
+	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();
+}

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();