diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java index f1585cee..5a4e8f41 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java @@ -12,6 +12,7 @@ public class RefinedFunction extends Refined { private String targetClass; private List stateChange; private String signature; + private PlacementInCode placementInCode; public RefinedFunction() { argRefinements = new ArrayList<>(); @@ -50,6 +51,14 @@ public String getSignature() { return signature; } + public void setPlacementInCode(CtElement element) { + placementInCode = PlacementInCode.createPlacement(element); + } + + public PlacementInCode getPlacementInCode() { + return placementInCode; + } + public Predicate getRenamedRefinements(Context c, CtElement element) { return getRenamedRefinements(getAllRefinements(), c, element); } 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 cbdca4a5..d9d6b2b5 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 @@ -43,6 +43,7 @@ public void getConstructorRefinements(CtConstructor c) throws LJError { RefinedFunction f = new RefinedFunction(); f.setName(c.getSimpleName()); f.setType(c.getType()); + f.setPlacementInCode(c); handleFunctionRefinements(f, c, c.getParameters()); f.setRefReturn(new Predicate()); CtTypeReference declaring = c.getDeclaringType() != null ? c.getDeclaringType().getReference() : null; @@ -79,6 +80,7 @@ public void getMethodRefinements(CtMethod method) throws LJError { f.setName(method.getSimpleName().replaceAll("\\p{C}", "")); // remove any empty chars from string f.setType(method.getType()); f.setRefReturn(new Predicate()); + f.setPlacementInCode(method); CtClass klass = null; if (method.getParent() instanceof CtClass) { @@ -116,6 +118,7 @@ public void getMethodRefinements(CtMethod method, String prefix) throws L f.setName(functionName.replaceAll("\\p{C}", "")); // remove any empty chars from string f.setType(method.getType()); f.setRefReturn(new Predicate()); + f.setPlacementInCode(method); f.setClass(prefix); f.setSignature(String.format("%s.%s", prefix, method.getSignature())); rtc.getContext().addFunctionToContext(f);