From 55bb7bc1bb3b03e821d78ad9c002559d462cc837 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 9 Oct 2026 00:08:59 +0100 Subject: [PATCH] Apply external contracts to inherited receiver methods --- .../JFrameRefinements.java | 18 +++++++++++ .../inherited_external_correct/UseFrame.java | 11 +++++++ .../JFrameRefinements.java | 18 +++++++++++ .../inherited_external_error/UseFrame.java | 11 +++++++ .../inherited_external_visibility/Base.java | 7 +++++ .../inherited_external_visibility/Child.java | 3 ++ .../ChildRefinements.java | 11 +++++++ .../DefaultChildRefinements.java | 12 ++++++++ .../StaticParent.java | 5 ++++ .../StackRefinements.java | 11 +++++++ .../inherited_overload_correct/UseStack.java | 12 ++++++++ .../StackRefinements.java | 11 +++++++ .../inherited_overload_error/UseStack.java | 12 ++++++++ .../inherited_source_correct/Base.java | 9 ++++++ .../inherited_source_correct/Child.java | 6 ++++ .../ChildRefinements.java | 11 +++++++ .../inherited_source_correct/UseChild.java | 17 +++++++++++ .../classes/inherited_source_error/Base.java | 9 ++++++ .../classes/inherited_source_error/Child.java | 6 ++++ .../ChildRefinements.java | 11 +++++++ .../inherited_source_error/UseChild.java | 17 +++++++++++ .../liquidjava/processor/context/Context.java | 8 ++++- .../ExternalRefinementTypeChecker.java | 30 +++++++++++++++++-- .../MethodsFunctionsChecker.java | 19 ++++++++++++ 24 files changed, 282 insertions(+), 3 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_external_correct/JFrameRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_external_correct/UseFrame.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_external_error/JFrameRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_external_error/UseFrame.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/Base.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/Child.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/ChildRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/DefaultChildRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/StaticParent.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_overload_correct/StackRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_overload_correct/UseStack.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_overload_error/StackRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_overload_error/UseStack.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/Base.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/Child.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/ChildRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/UseChild.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/Base.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/Child.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/ChildRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/UseChild.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_correct/JFrameRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_correct/JFrameRefinements.java new file mode 100644 index 000000000..e5fb37307 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_correct/JFrameRefinements.java @@ -0,0 +1,18 @@ +package testSuite.classes.inherited_external_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"displayable", "notDisplayable"}) +@ExternalRefinementsFor("javax.swing.JFrame") +public interface JFrameRefinements { + @StateRefinement(to = "notDisplayable(this)") + void JFrame(String title); + + @StateRefinement(to = "displayable(this)") + void pack(); + + @StateRefinement(from = "notDisplayable(this)") + void setUndecorated(boolean undecorated); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_correct/UseFrame.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_correct/UseFrame.java new file mode 100644 index 000000000..d6c6566bc --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_correct/UseFrame.java @@ -0,0 +1,11 @@ +package testSuite.classes.inherited_external_correct; + +import javax.swing.JFrame; + +public class UseFrame { + static void configure() { + JFrame frame = new JFrame("example"); + frame.setUndecorated(true); + frame.pack(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_error/JFrameRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_error/JFrameRefinements.java new file mode 100644 index 000000000..1c08cfab9 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_error/JFrameRefinements.java @@ -0,0 +1,18 @@ +package testSuite.classes.inherited_external_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"displayable", "notDisplayable"}) +@ExternalRefinementsFor("javax.swing.JFrame") +public interface JFrameRefinements { + @StateRefinement(to = "notDisplayable(this)") + void JFrame(String title); + + @StateRefinement(to = "displayable(this)") + void pack(); + + @StateRefinement(from = "notDisplayable(this)") + void setUndecorated(boolean undecorated); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_error/UseFrame.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_error/UseFrame.java new file mode 100644 index 000000000..22ee1218e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_error/UseFrame.java @@ -0,0 +1,11 @@ +package testSuite.classes.inherited_external_error; + +import javax.swing.JFrame; + +public class UseFrame { + static void configure() { + JFrame frame = new JFrame("example"); + frame.pack(); + frame.setUndecorated(true); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/Base.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/Base.java new file mode 100644 index 000000000..9a6f94f32 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/Base.java @@ -0,0 +1,7 @@ +package testSuite.classes.inherited_external_visibility.parent; + +public class Base { + private void privateMethod() {} + void packageMethod() {} + protected void protectedMethod() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/Child.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/Child.java new file mode 100644 index 000000000..3ec4be444 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/Child.java @@ -0,0 +1,3 @@ +package testSuite.classes.inherited_external_visibility; + +public class Child extends testSuite.classes.inherited_external_visibility.parent.Base implements StaticParent {} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/ChildRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/ChildRefinements.java new file mode 100644 index 000000000..3ba6f4b38 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/ChildRefinements.java @@ -0,0 +1,11 @@ +package testSuite.classes.inherited_external_visibility; + +import liquidjava.specification.ExternalRefinementsFor; + +@ExternalRefinementsFor("testSuite.classes.inherited_external_visibility.Child") +public interface ChildRefinements { + void privateMethod(); // Expect: Warning + void packageMethod(); // Expect: Warning + void interfaceStatic(); // Expect: Warning + void protectedMethod(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/DefaultChildRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/DefaultChildRefinements.java new file mode 100644 index 000000000..bae14779b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/DefaultChildRefinements.java @@ -0,0 +1,12 @@ +import liquidjava.specification.ExternalRefinementsFor; + +class DefaultParent { + void packageMethod() {} +} + +class DefaultChild extends DefaultParent {} + +@ExternalRefinementsFor("DefaultChild") +public interface DefaultChildRefinements { + void packageMethod(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/StaticParent.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/StaticParent.java new file mode 100644 index 000000000..f35827676 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/StaticParent.java @@ -0,0 +1,5 @@ +package testSuite.classes.inherited_external_visibility; + +public interface StaticParent { + static void interfaceStatic() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_correct/StackRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_correct/StackRefinements.java new file mode 100644 index 000000000..4179a0e5f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_correct/StackRefinements.java @@ -0,0 +1,11 @@ +package testSuite.classes.inherited_overload_correct; + +import liquidjava.specification.*; + +@ExternalRefinementsFor("java.util.Stack") +@StateSet({"ready", "changed"}) +public interface StackRefinements { + @StateRefinement(to = "ready(this)") void Stack(); + @StateRefinement(to = "changed(this)") E remove(int index); + @StateRefinement(from = "ready(this)") E peek(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_correct/UseStack.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_correct/UseStack.java new file mode 100644 index 000000000..8ee4445eb --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_correct/UseStack.java @@ -0,0 +1,12 @@ +package testSuite.classes.inherited_overload_correct; + +import java.util.Stack; + +public class UseStack { + static void check() { + Stack stack = new Stack<>(); + stack.add("value"); + stack.remove("value"); + stack.peek(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_error/StackRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_error/StackRefinements.java new file mode 100644 index 000000000..d0158bbfe --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_error/StackRefinements.java @@ -0,0 +1,11 @@ +package testSuite.classes.inherited_overload_error; + +import liquidjava.specification.*; + +@ExternalRefinementsFor("java.util.Stack") +@StateSet({"ready", "changed"}) +public interface StackRefinements { + @StateRefinement(to = "ready(this)") void Stack(); + @StateRefinement(to = "changed(this)") E remove(int index); + @StateRefinement(from = "ready(this)") E peek(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_error/UseStack.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_error/UseStack.java new file mode 100644 index 000000000..08e6c0261 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_error/UseStack.java @@ -0,0 +1,12 @@ +package testSuite.classes.inherited_overload_error; + +import java.util.Stack; + +public class UseStack { + static void check() { + Stack stack = new Stack<>(); + stack.add("value"); + stack.remove(0); + stack.peek(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/Base.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/Base.java new file mode 100644 index 000000000..4e920a01e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/Base.java @@ -0,0 +1,9 @@ +package testSuite.classes.inherited_source_correct; + +public class Base { + public void change(int value) {} + public void change(String value) {} + public void use() {} + public void inheritedPositive(@liquidjava.specification.Refinement("_ > 0") int value) {} + public void overridePositive(@liquidjava.specification.Refinement("_ > 0") int value) {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/Child.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/Child.java new file mode 100644 index 000000000..cc89e155d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/Child.java @@ -0,0 +1,6 @@ +package testSuite.classes.inherited_source_correct; + +public class Child extends Base { + @Override + public void overridePositive(@liquidjava.specification.Refinement("_ >= 0") int value) {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/ChildRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/ChildRefinements.java new file mode 100644 index 000000000..55edbf021 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/ChildRefinements.java @@ -0,0 +1,11 @@ +package testSuite.classes.inherited_source_correct; + +import liquidjava.specification.*; + +@ExternalRefinementsFor("testSuite.classes.inherited_source_correct.Child") +@StateSet({"ready", "changed"}) +public interface ChildRefinements { + @StateRefinement(to = "ready(this)") void Child(); + @StateRefinement(to = "changed(this)") void change(int value); + @StateRefinement(from = "ready(this)") void use(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/UseChild.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/UseChild.java new file mode 100644 index 000000000..37098da40 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/UseChild.java @@ -0,0 +1,17 @@ +package testSuite.classes.inherited_source_correct; + +public class UseChild { + static void check() { + Child child = new Child(); + child.change("unchanged"); + child.use(); + } + + static void superclassFallback() { + new Child().inheritedPositive(1); + } + + static void subclassOverride() { + new Child().overridePositive(0); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/Base.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/Base.java new file mode 100644 index 000000000..7f7ed5f57 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/Base.java @@ -0,0 +1,9 @@ +package testSuite.classes.inherited_source_error; + +public class Base { + public void change(int value) {} + public void change(String value) {} + public void use() {} + public void inheritedPositive(@liquidjava.specification.Refinement("_ > 0") int value) {} + public void overridePositive(@liquidjava.specification.Refinement("_ > 0") int value) {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/Child.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/Child.java new file mode 100644 index 000000000..7b22bbfb5 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/Child.java @@ -0,0 +1,6 @@ +package testSuite.classes.inherited_source_error; + +public class Child extends Base { + @Override + public void overridePositive(@liquidjava.specification.Refinement("_ >= 0") int value) {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/ChildRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/ChildRefinements.java new file mode 100644 index 000000000..918418f5b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/ChildRefinements.java @@ -0,0 +1,11 @@ +package testSuite.classes.inherited_source_error; + +import liquidjava.specification.*; + +@ExternalRefinementsFor("testSuite.classes.inherited_source_error.Child") +@StateSet({"ready", "changed"}) +public interface ChildRefinements { + @StateRefinement(to = "ready(this)") void Child(); + @StateRefinement(to = "changed(this)") void change(int value); + @StateRefinement(from = "ready(this)") void use(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/UseChild.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/UseChild.java new file mode 100644 index 000000000..e65c4a574 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/UseChild.java @@ -0,0 +1,17 @@ +package testSuite.classes.inherited_source_error; + +public class UseChild { + static void check() { + Child child = new Child(); + child.change(1); + child.use(); // Expect: State Refinement Error + } + + static void superclassFallback() { + new Child().inheritedPositive(-1); // Expect: Refinement Error + } + + static void subclassOverride() { + new Child().overridePositive(0); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index e8731991b..0334d15c0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -344,12 +344,18 @@ public RefinedFunction getFunction(String name, String target, int size) { } public RefinedFunction getFunction(String name, String target, List> paramTypes) { + RefinedFunction exact = getFunctionExact(name, target, paramTypes); + return exact != null ? exact : getFunction(name, target, paramTypes.size()); + } + + /** Looks up a receiver-specific contract without selecting a different overload by arity. */ + public RefinedFunction getFunctionExact(String name, String target, List> paramTypes) { for (RefinedFunction fi : ctxFunctions) { if (fi.getTargetClass() != null && fi.getName().equals(name) && fi.getTargetClass().equals(target) && argumentTypesMatch(fi.getArguments(), paramTypes)) return fi; } - return getFunction(name, target, paramTypes.size()); + return null; } private boolean argumentTypesMatch(List args, List> paramTypes) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 1339355c0..df5bb9762 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -2,6 +2,7 @@ import java.util.List; import java.util.Optional; +import java.util.stream.Stream; import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.LJError; @@ -140,11 +141,36 @@ private boolean classExists(String className) { private boolean methodExists(CtType targetType, CtMethod method) { // find method with matching signature - return targetType.getMethods().stream().filter(m -> m.getSimpleName().equals(method.getSimpleName())) + return inheritedMethods(targetType).filter(m -> m.getSimpleName().equals(method.getSimpleName())) .anyMatch(m -> parametersMatch(m.getParameters(), method.getParameters()) && typesMatch(m.getType(), method.getType())); } + /** Includes only methods that are declared on, or inherited by, the external target. */ + private Stream> inheritedMethods(CtType targetType) { + return targetType.getAllMethods().stream().filter(method -> { + CtType owner = method.getDeclaringType(); + if (owner == null) + return false; + if (owner.getQualifiedName().equals(targetType.getQualifiedName())) + return true; + if (method.isPrivate() || owner instanceof CtInterface && method.isStatic()) + return false; + if (method.isPublic() || method.isProtected()) + return true; + // A package-private method stops being inherited when a superclass crosses package boundaries. + CtType current = targetType; + while (current != null && !current.getQualifiedName().equals(owner.getQualifiedName())) { + if (current.getPackage() == null || owner.getPackage() == null + || !current.getPackage().getQualifiedName().equals(owner.getPackage().getQualifiedName())) + return false; + CtTypeReference parent = current.getSuperclass(); + current = parent == null ? null : parent.getTypeDeclaration(); + } + return current != null; + }); + } + private boolean constructorExists(CtType targetType, CtMethod method) { // find constructor with matching signature CtClass targetClass = (CtClass) targetType; @@ -188,7 +214,7 @@ private boolean parametersMatch(List targetParams, List refinementParams) } private String[] getOverloads(CtType targetType, CtMethod method) { - return targetType.getMethods().stream().filter(m -> m.getSimpleName().equals(method.getSimpleName())) + return inheritedMethods(targetType).filter(m -> m.getSimpleName().equals(method.getSimpleName())) .map(m -> String.format("%s %s", m.getType().getSimpleName(), m.getSignature())).toArray(String[]::new); } } 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 88a379369..57c0b0310 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 @@ -233,6 +233,8 @@ public void getReturnRefinements(CtReturn ret) throws LJError { // ################################ public void getInvocationRefinements(CtInvocation invocation) throws LJError { + if (tryReceiverRefinements(invocation)) + return; CtExecutable method = invocation.getExecutable().getDeclaration(); if (method == null) { @@ -252,6 +254,23 @@ public void getInvocationRefinements(CtInvocation invocation) throws LJEr } } + private boolean tryReceiverRefinements(CtInvocation invocation) throws LJError { + CtExpression receiver = invocation.getTarget(); + if (receiver == null || receiver.getType() == null) + return false; + String receiverType = receiver.getType().getQualifiedName(); + CtExecutableReference executable = invocation.getExecutable(); + for (String key : List.of(Utils.qualifyName(receiverType, executable.getSignature()), executable.getSignature(), + executable.getSimpleName(), Utils.qualifyName(receiverType, executable.getSimpleName()))) { + if (rtc.getContext().getFunctionExact(key, receiverType, executable.getParameters()) != null) { + checkInvocationRefinements(invocation, invocation.getArguments(), receiver, key, receiverType, + executable.getParameters()); + return true; + } + } + return false; + } + private void searchMethodInLibrary(CtExecutableReference ctr, CtInvocation invocation) throws LJError { CtTypeReference ctref = ctr.getDeclaringType(); if (ctref == null) {