From dbaa21298724ecbfce03bd0a86bd1d9ee404ea51 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 4 Nov 2026 18:48:31 +0000 Subject: [PATCH] Name refined call results after the method, as the other generated values MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The result of a call to a method with a contract was named #_N and shown as getUndoManager⁵⁵⁵, like a program variable. It is now a generated name, #getUndoManager_result⁵⁵⁵, as the results of the calls inside an expression already were. Co-Authored-By: Claude Opus 5.5 --- .../general_checkers/MethodsFunctionsChecker.java | 11 ++++++----- .../java/liquidjava/api/tests/TestGeneratedNames.java | 6 +++--- 2 files changed, 9 insertions(+), 8 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 272c1e83..74233c3e 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 @@ -16,6 +16,7 @@ import liquidjava.processor.refinement_checker.object_checkers.AuxHierarchyRefinementsPassage; import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler; import liquidjava.rj_language.Predicate; +import liquidjava.utils.GeneratedNames; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; @@ -330,7 +331,7 @@ private boolean tryRefinements(CtInvocation invocation, String key, String ct return true; } - private Map checkInvocationRefinements(CtElement invocation, List> arguments, + private Map checkInvocationRefinements(CtExpression invocation, List> arguments, CtExpression target, String methodName, String className, List> paramTypes) throws LJError { // -- Part 1: Check if the invocation is possible @@ -373,11 +374,11 @@ private Map checkInvocationRefinements(CtElement invocation, Lis * matches the post-call VariableInstance. Returns {@code null} for void methods. When the function has no * refinements to check, the (empty) instance is registered eagerly. */ - private String prepareReturnInstance(CtElement invocation, RefinedFunction f) { + private String prepareReturnInstance(CtExpression invocation, RefinedFunction f) { CtTypeReference retType = f.getType(); if (retType == null || "void".equals(retType.toString())) return null; - String returnViName = String.format(Formats.INSTANCE, f.getName(), rtc.getContext().getCounter()); + String returnViName = GeneratedNames.valueOf(invocation, rtc.getContext().getCounter()); invocation.putMetadata(Keys.RETURN_VAR_NAME, returnViName); if (f.allRefinementsTrue()) rtc.getContext().addInstanceToContext(returnViName, retType, new Predicate(), invocation); @@ -388,7 +389,7 @@ private String prepareReturnInstance(CtElement invocation, RefinedFunction f) { * Part 2 of an invocation check: applies the function's return refinement to the context, substituting argument and * target variables and registering the resulting return-value instance. */ - private void applyReturnRefinement(CtElement invocation, RefinedFunction f, Map map, + private void applyReturnRefinement(CtExpression invocation, RefinedFunction f, Map map, String returnViName) { Predicate methodRef = f.getRefReturn(); if (methodRef == null) @@ -410,7 +411,7 @@ private void applyReturnRefinement(CtElement invocation, RefinedFunction f, Map< } String viName = returnViName != null ? returnViName - : String.format(Formats.INSTANCE, f.getName(), rtc.getContext().getCounter()); + : GeneratedNames.valueOf(invocation, rtc.getContext().getCounter()); VariableInstance vi = (VariableInstance) rtc.getContext().addInstanceToContext(viName, f.getType(), methodRef.substituteVariable(Keys.WILDCARD, viName), invocation); // TODO REVIEW!! if (varName != null && f.hasStateChange() && equalsThis) diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java index 86e3fc00..c0d16143 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java @@ -22,9 +22,9 @@ void namesEachGeneratedValueAfterWhatItIs() { Map messages = Diagnostics.getInstance().getErrors().stream().collect(Collectors.toMap( error -> error.getPosition().getLine(), error -> error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""))); - assertEquals(Map.of(25, "#if_condition == ready && #if_condition is not a subtype of a > 0", 30, - "#loop_condition == ready && #loop_condition == true is not a subtype of a > 0", 34, - "#ternary_condition == ready && #ternary_condition == true is not a subtype of a < 0", 43, + assertEquals(Map.of(25, "#if_condition == #ready_result && #if_condition is not a subtype of a > 0", 30, + "#loop_condition == #ready_result && #loop_condition == true is not a subtype of a > 0", 34, + "#ternary_condition == #ready_result && #ternary_condition == true is not a subtype of a < 0", 43, "!#try_branch && !#catch_branch is not a subtype of a > 0", 48, "x == #read_result - 1 is not a subtype of x > 0", 54, "#if_condition == #operation_result && #if_condition && x == 0 is not a subtype of x > 0", 58,