From 8daedfd84217d52c5041e1a39f3b761c0e7362c5 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 10 Mar 2026 05:24:29 +0000 Subject: [PATCH 1/2] Initial plan From e372735f2643f4a0486604ff4f2808b522346d10 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 10 Mar 2026 05:29:36 +0000 Subject: [PATCH 2/2] Fix getReturnRefinements to use type-based lookup for method overloads and extract helper method Co-authored-by: CatarinaGamboa <52540187+CatarinaGamboa@users.noreply.github.com> --- .../MethodsFunctionsChecker.java | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 688ca2e4..661460f0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -184,8 +184,11 @@ public void getReturnRefinements(CtReturn ret) throws LJError { if (rtc.getRefinement(method) == null) return; if (method.getParent() instanceof CtClass) { - RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), - ((CtClass) method.getParent()).getQualifiedName(), method.getParameters().size()); + List> paramTypes = extractParameterTypes(method.getParameters()); + String parentClass = ((CtClass) method.getParent()).getQualifiedName(); + RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), parentClass, paramTypes); + if (fi == null) + fi = rtc.getContext().getFunction(method.getSimpleName(), parentClass, method.getParameters().size()); if (fi == null) return; @@ -440,6 +443,13 @@ private void applyRefinementsToArguments(CtElement element, List } } + private List> extractParameterTypes(List> parameters) { + List> paramTypes = new ArrayList<>(); + for (CtParameter p : parameters) + paramTypes.add(p.getType()); + return paramTypes; + } + public void loadFunctionInfo(CtExecutable method) { String className = null; if (method.getParent() instanceof CtClass) { @@ -448,9 +458,7 @@ public void loadFunctionInfo(CtExecutable method) { className = ((CtInterface) method.getParent()).getQualifiedName(); } if (className != null) { - List> paramTypes = new ArrayList<>(); - for (CtParameter p : method.getParameters()) - paramTypes.add(p.getType()); + List> paramTypes = extractParameterTypes(method.getParameters()); RefinedFunction fi = getRefinementFunction(method.getSimpleName(), className, paramTypes); if (fi != null) { List lv = fi.getArguments();