Fix Refined Method Overloading

Co-Authored-By: Márcio Caetano <153174341+rodrigomilisse@users.noreply.github.com>

Author: rcosta358

liquidjava-example/src/main/java/testSuite/classes/method_overload_correct/DummySemaphoreRefinements.java

@@ -0,0 +1,12 @@
+package testSuite.classes.method_overload_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+
+@ExternalRefinementsFor("java.util.concurrent.Semaphore")
+public interface DummySemaphoreRefinements {
+
+	public abstract void acquire();
+
+	public abstract void acquire(@Refinement("_ >= 0") int permits) throws InterruptedException;
+}

liquidjava-example/src/main/java/testSuite/classes/method_overload_correct/TestMethodOverloadCorrect.java

@@ -0,0 +1,10 @@
+package testSuite.classes.method_overload_correct;
+
+import java.util.concurrent.Semaphore;
+
+public class TestMethodOverloadCorrect {
+	public static void main(String[] args) throws InterruptedException {
+		Semaphore sem = new Semaphore(1);
+		sem.acquire(1);
+	}
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java

@@ -191,7 +191,7 @@ public <R> void getReturnRefinements(CtReturn<R> ret) {
                 return;
             if (method.getParent() instanceof CtClass) {
                 RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(),
-                        ((CtClass<?>) method.getParent()).getQualifiedName());
+                        ((CtClass<?>) method.getParent()).getQualifiedName(), method.getParameters().size());
 
                 List<Variable> lv = fi.getArguments();
                 for (Variable v : lv) {
@@ -229,7 +229,8 @@ public <R> void getInvocationRefinements(CtInvocation<R> invocation) {
 
         } else if (method.getParent() instanceof CtClass) {
             String ctype = ((CtClass<?>) method.getParent()).getQualifiedName();
-            RefinedFunction f = rtc.getContext().getFunction(method.getSimpleName(), ctype);
+            int argSize = invocation.getArguments().size();
+            RefinedFunction f = rtc.getContext().getFunction(method.getSimpleName(), ctype, argSize);
             if (f != null) { // inside rtc.context
                 checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(),
                         method.getSimpleName(), ctype);
@@ -264,13 +265,14 @@ private void searchMethodInLibrary(CtExecutableReference<?> ctr, CtInvocation<?>
         String ctype = (ctref != null) ? ctref.toString() : null;
 
         String name = ctr.getSimpleName(); // missing
-        if (rtc.getContext().getFunction(name, ctype) != null) { // inside rtc.context
+        int argSize = invocation.getArguments().size();
+        if (rtc.getContext().getFunction(name, ctype, argSize) != null) { // inside rtc.context
             checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), name, ctype);
             return;
         } else {
             String prefix = ctype;
             String completeName = String.format("%s.%s", prefix, name);
-            if (rtc.getContext().getFunction(completeName, ctype) != null) {
+            if (rtc.getContext().getFunction(completeName, ctype, argSize) != null) {
                 checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), completeName,
                         ctype);
             }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java

@@ -249,7 +249,7 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
 
             // Get function refinements with non_used variables
             String met = ((CtClass<?>) method.getParent()).getQualifiedName(); // TODO check
-            RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), met);
+            RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), met, inv.getArguments().size());
             Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVER!!
             // Substitute _ by the variable that we send
             String newName = String.format(rtc.freshFormat, rtc.getContext().getCounter());
@@ -275,7 +275,8 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation<?> inv, CtB
             int i = c.indexOf("<");
             String typeNotParametrized = (i > 0) ? c.substring(0, i) : c;
             String methodInClassName = typeNotParametrized + "." + simpleName;
-            RefinedFunction fi = rtc.getContext().getFunction(methodInClassName, typeNotParametrized);
+            RefinedFunction fi = rtc.getContext().getFunction(methodInClassName, typeNotParametrized,
+                    inv.getArguments().size());
             Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVER!!
 
             // Substitute _ by the variable that we send