From 9024b64a341cbe2161cc1a1553aeffd716a4956e Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 10 May 2026 18:09:57 +0100 Subject: [PATCH 1/2] Add Methods to Context History --- .../processor/context/ContextHistory.java | 8 ++++++++ .../processor/context/RefinedFunction.java | 13 +++++++++++++ .../general_checkers/MethodsFunctionsChecker.java | 3 +++ 3 files changed, 24 insertions(+) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java index f2274476..88b49687 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -17,6 +17,7 @@ public class ContextHistory { private Set ghosts; private Set aliases; private Set globalVars; + private Set methods; private ContextHistory() { fileScopes = new HashMap<>(); @@ -24,6 +25,7 @@ private ContextHistory() { globalVars = new HashSet<>(); ghosts = new HashSet<>(); aliases = new HashSet<>(); + methods = new HashSet<>(); } public static ContextHistory getInstance() { @@ -38,6 +40,7 @@ public void clearHistory() { globalVars.clear(); ghosts.clear(); aliases.clear(); + methods.clear(); } public void saveContext(CtElement element, Context context) { @@ -56,6 +59,7 @@ public void saveContext(CtElement element, Context context) { globalVars.addAll(context.getCtxGlobalVars()); ghosts.addAll(context.getGhostStates()); aliases.addAll(context.getAliases()); + methods.addAll(context.getCtxFunctions()); } private String getScopePosition(CtElement element) { @@ -81,6 +85,10 @@ public Set getAliases() { return aliases; } + public Set getMethods() { + return methods; + } + public Map> getFileScopes() { return fileScopes; } 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..e3a59bed 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,18 @@ public String getSignature() { return signature; } + public void setPlacementInCode(CtElement element) { + placementInCode = PlacementInCode.createPlacement(element); + } + + public void setPlacementInScope(PlacementInCode placement) { + placementInCode = placement; + } + + 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..29df612e 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; @@ -78,6 +79,7 @@ public void getMethodRefinements(CtMethod method) throws LJError { RefinedFunction f = new RefinedFunction(); f.setName(method.getSimpleName().replaceAll("\\p{C}", "")); // remove any empty chars from string f.setType(method.getType()); + f.setPlacementInCode(method); f.setRefReturn(new Predicate()); CtClass klass = null; @@ -115,6 +117,7 @@ public void getMethodRefinements(CtMethod method, String prefix) throws L RefinedFunction f = new RefinedFunction(); f.setName(functionName.replaceAll("\\p{C}", "")); // remove any empty chars from string f.setType(method.getType()); + f.setPlacementInCode(method); f.setRefReturn(new Predicate()); f.setClass(prefix); f.setSignature(String.format("%s.%s", prefix, method.getSignature())); From 747fcd38e9f4aaeecdc68a4a8c0705e979cf38f2 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 10 May 2026 18:25:43 +0100 Subject: [PATCH 2/2] Remove Positions --- .../processor/context/RefinedFunction.java | 13 ------------- .../refinement_checker/RefinementTypeChecker.java | 2 +- .../general_checkers/MethodsFunctionsChecker.java | 3 --- 3 files changed, 1 insertion(+), 17 deletions(-) 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 e3a59bed..f1585cee 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java @@ -12,7 +12,6 @@ public class RefinedFunction extends Refined { private String targetClass; private List stateChange; private String signature; - private PlacementInCode placementInCode; public RefinedFunction() { argRefinements = new ArrayList<>(); @@ -51,18 +50,6 @@ public String getSignature() { return signature; } - public void setPlacementInCode(CtElement element) { - placementInCode = PlacementInCode.createPlacement(element); - } - - public void setPlacementInScope(PlacementInCode placement) { - placementInCode = placement; - } - - 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/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 09095f35..e5655d5a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -379,7 +379,7 @@ public void visitCtIf(CtIf ifElement) { thenRefs = Predicate.createConjunction(expRefs, freshIsTrue); elseRefs = Predicate.createConjunction(expRefs, freshIsFalse); } - + freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp); } vcChecker.addPathVariable(freshRV); 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 29df612e..cbdca4a5 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,7 +43,6 @@ 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,7 +78,6 @@ public void getMethodRefinements(CtMethod method) throws LJError { RefinedFunction f = new RefinedFunction(); f.setName(method.getSimpleName().replaceAll("\\p{C}", "")); // remove any empty chars from string f.setType(method.getType()); - f.setPlacementInCode(method); f.setRefReturn(new Predicate()); CtClass klass = null; @@ -117,7 +115,6 @@ public void getMethodRefinements(CtMethod method, String prefix) throws L RefinedFunction f = new RefinedFunction(); f.setName(functionName.replaceAll("\\p{C}", "")); // remove any empty chars from string f.setType(method.getType()); - f.setPlacementInCode(method); f.setRefReturn(new Predicate()); f.setClass(prefix); f.setSignature(String.format("%s.%s", prefix, method.getSignature()));