Fix Inconsistent Qualified Names

liquidjava-example/src/main/java/testSuite/classes/conflicting_ghost_names_correct/SimpleTest.java

@@ -10,8 +10,10 @@ public void example() {
         list.get(0);
 
         Stack<Integer> stack = new Stack<>();
-		stack.push(1);
-		stack.peek();
+		if (stack.empty()) {
+			stack.push(1);
+            stack.peek();
+		}
 		stack.pop();
     }
 }

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<E> {
 
 	@StateRefinement(from="size(this) > 0")
 	public E peek();
+
+	@Refinement("_ ? size(this) == 0 : size(this) > 0")
+	public boolean empty();
 }

liquidjava-verifier/pom.xml

@@ -11,7 +11,7 @@
 
 	<groupId>io.github.liquid-java</groupId>
 	<artifactId>liquidjava-verifier</artifactId>
-	<version>0.0.27</version>
+	<version>0.0.28</version>
 	<name>liquidjava-verifier</name>
 	<description>LiquidJava Verifier</description>
 	<url>https://github.com/liquid-java/liquidjava</url>

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -105,7 +105,9 @@ public Optional<Predicate> 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",

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