From fcaa941b140bad10b3af753d82e9ba6e172582df Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 18 Feb 2026 18:49:56 +0000 Subject: [PATCH 1/7] Save Context History --- .../processor/context/ContextHistory.java | 35 +++++-------------- 1 file changed, 9 insertions(+), 26 deletions(-) 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 0e4db162..70b5c4d1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -7,19 +7,18 @@ import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; -import spoon.reflect.declaration.CtExecutable; public class ContextHistory { private static ContextHistory instance; - - private Map>> fileScopeVars; // file -> (scope -> variables in scope) + + private Map> vars; // scope -> variables in scope private Set instanceVars; private Set globalVars; private Set ghosts; private Set aliases; private ContextHistory() { - fileScopeVars = new HashMap<>(); + vars = new HashMap<>(); instanceVars = new HashSet<>(); globalVars = new HashSet<>(); ghosts = new HashSet<>(); @@ -33,7 +32,7 @@ public static ContextHistory getInstance() { } public void clearHistory() { - fileScopeVars.clear(); + vars.clear(); instanceVars.clear(); globalVars.clear(); ghosts.clear(); @@ -44,33 +43,17 @@ public void saveContext(CtElement element, Context context) { SourcePosition pos = element.getPosition(); if (pos == null || pos.getFile() == null) return; - - // add variables in scope for this position - String file = pos.getFile().getAbsolutePath(); - String scope = getScopePosition(element); - fileScopeVars.putIfAbsent(file, new HashMap<>()); - fileScopeVars.get(file).put(scope, new HashSet<>(context.getCtxVars())); - - // add other elements in context + + String scope = String.format("%s:%d:%d", pos.getFile().getName(), pos.getLine(), pos.getColumn()); + vars.put(scope, new HashSet<>(context.getCtxVars())); instanceVars.addAll(context.getCtxInstanceVars()); globalVars.addAll(context.getCtxGlobalVars()); ghosts.addAll(context.getGhostStates()); aliases.addAll(context.getAliases()); } - public String getScopePosition(CtElement element) { - SourcePosition pos = element.getPosition(); - SourcePosition innerPosition = pos; - if (element instanceof CtExecutable executable) { - if (executable.getBody() != null) - innerPosition = executable.getBody().getPosition(); - } - return String.format("%d:%d-%d:%d", innerPosition.getLine(), innerPosition.getColumn() + 1, pos.getEndLine(), - pos.getEndColumn()); - } - - public Map>> getFileScopeVars() { - return fileScopeVars; + public Map> getVars() { + return vars; } public Set getInstanceVars() { From a532c05a17806af02a41b8a421a9aaa414691414 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 19 Feb 2026 14:27:29 +0000 Subject: [PATCH 2/7] Save Context Vars by File and Scope --- .../processor/context/ContextHistory.java | 22 +++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) 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 70b5c4d1..df54651d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -7,11 +7,13 @@ import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; +import spoon.reflect.declaration.CtExecutable; +import spoon.reflect.declaration.CtMethod; public class ContextHistory { private static ContextHistory instance; - private Map> vars; // scope -> variables in scope + private Map>> vars; // file -> (scope -> variables in scope) private Set instanceVars; private Set globalVars; private Set ghosts; @@ -43,16 +45,28 @@ public void saveContext(CtElement element, Context context) { SourcePosition pos = element.getPosition(); if (pos == null || pos.getFile() == null) return; + + // add variables in scope for this position + String file = pos.getFile().getAbsolutePath(); + String scope = getScopePosition(element); + System.out.println("Saving context for " + file + " in scope " + scope); + vars.putIfAbsent(file, new HashMap<>()); + vars.get(file).put(scope, new HashSet<>(context.getCtxVars())); - String scope = String.format("%s:%d:%d", pos.getFile().getName(), pos.getLine(), pos.getColumn()); - vars.put(scope, new HashSet<>(context.getCtxVars())); + // add other elements in context instanceVars.addAll(context.getCtxInstanceVars()); globalVars.addAll(context.getCtxGlobalVars()); ghosts.addAll(context.getGhostStates()); aliases.addAll(context.getAliases()); } - public Map> getVars() { + public String getScopePosition(CtElement element) { + SourcePosition pos = element.getPosition(); + SourcePosition innerPosition = element instanceof CtExecutable ? ((CtExecutable) element).getBody().getPosition() : pos; + return String.format("%d:%d-%d:%d", innerPosition.getLine(), innerPosition.getColumn() + 1, pos.getEndLine(), pos.getEndColumn()); + } + + public Map>> getVars() { return vars; } From 07a4c631ae5d7340d7a47ecd2413a7ca985d4fc9 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 19 Feb 2026 15:48:25 +0000 Subject: [PATCH 3/7] Fix NPE --- .../processor/context/ContextHistory.java | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) 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 df54651d..b3670130 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -8,11 +8,10 @@ import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtExecutable; -import spoon.reflect.declaration.CtMethod; public class ContextHistory { private static ContextHistory instance; - + private Map>> vars; // file -> (scope -> variables in scope) private Set instanceVars; private Set globalVars; @@ -49,10 +48,9 @@ public void saveContext(CtElement element, Context context) { // add variables in scope for this position String file = pos.getFile().getAbsolutePath(); String scope = getScopePosition(element); - System.out.println("Saving context for " + file + " in scope " + scope); vars.putIfAbsent(file, new HashMap<>()); vars.get(file).put(scope, new HashSet<>(context.getCtxVars())); - + // add other elements in context instanceVars.addAll(context.getCtxInstanceVars()); globalVars.addAll(context.getCtxGlobalVars()); @@ -62,8 +60,13 @@ public void saveContext(CtElement element, Context context) { public String getScopePosition(CtElement element) { SourcePosition pos = element.getPosition(); - SourcePosition innerPosition = element instanceof CtExecutable ? ((CtExecutable) element).getBody().getPosition() : pos; - return String.format("%d:%d-%d:%d", innerPosition.getLine(), innerPosition.getColumn() + 1, pos.getEndLine(), pos.getEndColumn()); + SourcePosition innerPosition = pos; + if (element instanceof CtExecutable executable) { + if (executable.getBody() != null) + innerPosition = executable.getBody().getPosition(); + } + return String.format("%d:%d-%d:%d", innerPosition.getLine(), innerPosition.getColumn() + 1, pos.getEndLine(), + pos.getEndColumn()); } public Map>> getVars() { From dd127c687615fcebd7d63c141e90644018bf4ece Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 20 Feb 2026 19:08:53 +0000 Subject: [PATCH 4/7] Save Ghosts By File --- .../processor/context/ContextHistory.java | 36 +++++++++++++------ .../ExternalRefinementTypeChecker.java | 6 ++-- .../refinement_checker/TypeChecker.java | 4 +++ 3 files changed, 34 insertions(+), 12 deletions(-) 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 b3670130..b16f3ef2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -13,16 +13,18 @@ public class ContextHistory { private static ContextHistory instance; private Map>> vars; // file -> (scope -> variables in scope) + private Map> ghosts; // file -> ghosts + + // globals + private Set aliases; private Set instanceVars; private Set globalVars; - private Set ghosts; - private Set aliases; private ContextHistory() { vars = new HashMap<>(); instanceVars = new HashSet<>(); globalVars = new HashSet<>(); - ghosts = new HashSet<>(); + ghosts = new HashMap<>(); aliases = new HashSet<>(); } @@ -41,23 +43,37 @@ public void clearHistory() { } public void saveContext(CtElement element, Context context) { - SourcePosition pos = element.getPosition(); - if (pos == null || pos.getFile() == null) + String file = getFile(element); + if (file == null) return; - // add variables in scope for this position - String file = pos.getFile().getAbsolutePath(); + // add variables in scope String scope = getScopePosition(element); vars.putIfAbsent(file, new HashMap<>()); vars.get(file).put(scope, new HashSet<>(context.getCtxVars())); - // add other elements in context + // add other elements in context (except ghosts) instanceVars.addAll(context.getCtxInstanceVars()); globalVars.addAll(context.getCtxGlobalVars()); - ghosts.addAll(context.getGhostStates()); aliases.addAll(context.getAliases()); } + public void saveGhost(CtElement element, GhostState ghost) { + String file = getFile(element); + if (file == null) + return; + ghosts.putIfAbsent(file, new HashSet<>()); + ghosts.get(file).add(ghost); + } + + private String getFile(CtElement element) { + SourcePosition pos = element.getPosition(); + if (pos == null || pos.getFile() == null) + return null; + + return pos.getFile().getAbsolutePath(); + } + public String getScopePosition(CtElement element) { SourcePosition pos = element.getPosition(); SourcePosition innerPosition = pos; @@ -81,7 +97,7 @@ public Set getGlobalVars() { return globalVars; } - public Set getGhosts() { + public Map> getGhosts() { return ghosts; } 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 154e94d0..aea227bf 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 @@ -8,6 +8,7 @@ import liquidjava.diagnostics.warnings.ExternalClassNotFoundWarning; import liquidjava.diagnostics.warnings.ExternalMethodNotFoundWarning; import liquidjava.processor.context.Context; +import liquidjava.processor.context.ContextHistory; import liquidjava.processor.context.GhostFunction; import liquidjava.processor.facade.GhostDTO; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; @@ -27,8 +28,9 @@ import spoon.reflect.reference.CtTypeReference; public class ExternalRefinementTypeChecker extends TypeChecker { - String prefix; - Diagnostics diagnostics = Diagnostics.getInstance(); + private String prefix; + private final Diagnostics diagnostics = Diagnostics.getInstance(); + private final ContextHistory contextHistory = ContextHistory.getInstance(); public ExternalRefinementTypeChecker(Context context, Factory factory) { super(context, factory); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index ac2abb2d..17baf88a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -9,6 +9,7 @@ import liquidjava.diagnostics.errors.*; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; +import liquidjava.processor.context.ContextHistory; import liquidjava.processor.context.GhostFunction; import liquidjava.processor.context.GhostState; import liquidjava.processor.context.RefinedVariable; @@ -40,6 +41,7 @@ public abstract class TypeChecker extends CtScanner { protected final Context context; protected final Factory factory; protected final VCChecker vcChecker; + private final ContextHistory contextHistory = ContextHistory.getInstance(); public TypeChecker(Context context, Factory factory) { this.context = context; @@ -158,6 +160,7 @@ private void createStateSet(CtNewArray e, int set, CtElement element) th gs.setRefinement(Predicate.createEquals(ip, Predicate.createLit(Integer.toString(order), Types.INT))); // open(THIS) -> state1(THIS) == 1 context.addToGhostClass(g.getParentClassName(), gs); + contextHistory.saveGhost(element, gs); } order++; } @@ -183,6 +186,7 @@ private void createStateGhost(String string, CtAnnotation CtTypeReference r = factory.Type().createReference(gd.returnType()); GhostState gs = new GhostState(gd.name(), param, r, qn); context.addToGhostClass(sn, gs); + contextHistory.saveGhost(element, gs); } protected String getQualifiedClassName(CtElement element) { From eff70674c1f6600ea2081349adf2be789755f429 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 24 Feb 2026 13:27:04 +0000 Subject: [PATCH 5/7] Use Annotation Position & Mark Parameters This is needed to suggest parameters in method and parameter refinements --- .../main/java/liquidjava/diagnostics/LJDiagnostic.java | 2 +- .../liquidjava/processor/context/ContextHistory.java | 9 +++------ .../liquidjava/processor/context/RefinedVariable.java | 10 ++++++++++ .../general_checkers/MethodsFunctionsChecker.java | 1 + .../src/main/java/liquidjava/utils/Utils.java | 10 ++++++++++ 5 files changed, 25 insertions(+), 7 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 1c548648..d1a743dc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -129,7 +129,7 @@ public String getSnippet() { // line number padding + pipe + column offset String indent = " ".repeat(padding) + Colors.GREY + PIPE + Colors.RESET - + " ".repeat(visualColStart - 1); + + " ".repeat(visualColStart - 1); String markers = accentColor + "^".repeat(Math.max(1, visualColEnd - visualColStart + 1)); sb.append(indent).append(markers); 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 b16f3ef2..597c647e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -5,6 +5,7 @@ import java.util.Map; import java.util.Set; +import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtExecutable; @@ -76,12 +77,8 @@ private String getFile(CtElement element) { public String getScopePosition(CtElement element) { SourcePosition pos = element.getPosition(); - SourcePosition innerPosition = pos; - if (element instanceof CtExecutable executable) { - if (executable.getBody() != null) - innerPosition = executable.getBody().getPosition(); - } - return String.format("%d:%d-%d:%d", innerPosition.getLine(), innerPosition.getColumn() + 1, pos.getEndLine(), + SourcePosition annPosition = Utils.getFirstAnnotationPosition(element); + return String.format("%d:%d-%d:%d", annPosition.getLine(), annPosition.getColumn() + 1, pos.getEndLine(), pos.getEndColumn()); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java index 534f8cfa..9f57bb6e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java @@ -9,10 +9,12 @@ public abstract class RefinedVariable extends Refined { private final List> supertypes; private PlacementInCode placementInCode; + private boolean isParameter; public RefinedVariable(String name, CtTypeReference type, Predicate c) { super(name, type, c); supertypes = new ArrayList<>(); + isParameter = false; } public abstract Predicate getMainRefinement(); @@ -65,4 +67,12 @@ public boolean equals(Object obj) { return supertypes.equals(other.supertypes); } } + + public void setIsParameter(boolean b) { + isParameter = b; + } + + public boolean isParameter() { + return isParameter; + } } 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 af16bf92..1f1decda 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 @@ -154,6 +154,7 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method, c = oc.get().substituteVariable(Keys.WILDCARD, paramName); param.putMetadata(Keys.REFINEMENT, c); RefinedVariable v = rtc.getContext().addVarToContext(param.getSimpleName(), param.getType(), c, param); + v.setIsParameter(true); rtc.getMessageFromAnnotation(param).ifPresent(v::setMessage); if (v instanceof Variable) f.addArgRefinements((Variable) v); diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 1e99e3f0..069e007f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -44,6 +44,16 @@ public static SourcePosition getAnnotationPosition(CtElement element, String ref .map(CtElement::getPosition).orElse(element.getPosition()); } + public static SourcePosition getFirstAnnotationPosition(CtElement element) { + CtElement target = element.getParent() != null ? element.getParent() : element; + return target.getAnnotations().stream().filter(Utils::isLiquidJavaAnnotation).map(CtElement::getPosition) + .min((p1, p2) -> { + if (p1.getLine() != p2.getLine()) + return Integer.compare(p1.getLine(), p2.getLine()); + return Integer.compare(p1.getColumn(), p2.getColumn()); + }).orElse(target.getPosition()); + } + private static boolean isLiquidJavaAnnotation(CtAnnotation annotation) { return annotation.getAnnotationType().getQualifiedName().startsWith("liquidjava.specification"); } From 8ee09ea0a4ea570fa2a41158cb3ad1fe1cf33d04 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 24 Feb 2026 14:30:29 +0000 Subject: [PATCH 6/7] Fix --- .../processor/context/ContextHistory.java | 4 +++- .../src/main/java/liquidjava/utils/Utils.java | 13 ++++++------- 2 files changed, 9 insertions(+), 8 deletions(-) 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 597c647e..a28781e2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -9,6 +9,7 @@ import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtExecutable; +import spoon.reflect.declaration.CtParameter; public class ContextHistory { private static ContextHistory instance; @@ -76,8 +77,9 @@ private String getFile(CtElement element) { } public String getScopePosition(CtElement element) { + CtElement startElement = element instanceof CtParameter ? element.getParent() : element; + SourcePosition annPosition = Utils.getFirstAnnotationPosition(startElement); SourcePosition pos = element.getPosition(); - SourcePosition annPosition = Utils.getFirstAnnotationPosition(element); return String.format("%d:%d-%d:%d", annPosition.getLine(), annPosition.getColumn() + 1, pos.getEndLine(), pos.getEndColumn()); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 069e007f..e0b46507 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -45,13 +45,12 @@ public static SourcePosition getAnnotationPosition(CtElement element, String ref } public static SourcePosition getFirstAnnotationPosition(CtElement element) { - CtElement target = element.getParent() != null ? element.getParent() : element; - return target.getAnnotations().stream().filter(Utils::isLiquidJavaAnnotation).map(CtElement::getPosition) - .min((p1, p2) -> { - if (p1.getLine() != p2.getLine()) - return Integer.compare(p1.getLine(), p2.getLine()); - return Integer.compare(p1.getColumn(), p2.getColumn()); - }).orElse(target.getPosition()); + return element.getAnnotations().stream().filter(Utils::isLiquidJavaAnnotation).map(CtElement::getPosition) + .min((p1, p2) -> { + if (p1.getLine() != p2.getLine()) + return Integer.compare(p1.getLine(), p2.getLine()); + return Integer.compare(p1.getColumn(), p2.getColumn()); + }).orElse(element.getPosition()); } private static boolean isLiquidJavaAnnotation(CtAnnotation annotation) { From e74d105ce08c6b66ef953805390eab7abcce218f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 26 Feb 2026 11:07:11 +0000 Subject: [PATCH 7/7] Rename `fileScopeVars` --- .../processor/context/ContextHistory.java | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) 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 a28781e2..f969ebe3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -14,7 +14,7 @@ public class ContextHistory { private static ContextHistory instance; - private Map>> vars; // file -> (scope -> variables in scope) + private Map>> fileScopeVars; // file -> (scope -> variables in scope) private Map> ghosts; // file -> ghosts // globals @@ -23,7 +23,7 @@ public class ContextHistory { private Set globalVars; private ContextHistory() { - vars = new HashMap<>(); + fileScopeVars = new HashMap<>(); instanceVars = new HashSet<>(); globalVars = new HashSet<>(); ghosts = new HashMap<>(); @@ -37,7 +37,7 @@ public static ContextHistory getInstance() { } public void clearHistory() { - vars.clear(); + fileScopeVars.clear(); instanceVars.clear(); globalVars.clear(); ghosts.clear(); @@ -51,8 +51,8 @@ public void saveContext(CtElement element, Context context) { // add variables in scope String scope = getScopePosition(element); - vars.putIfAbsent(file, new HashMap<>()); - vars.get(file).put(scope, new HashSet<>(context.getCtxVars())); + fileScopeVars.putIfAbsent(file, new HashMap<>()); + fileScopeVars.get(file).put(scope, new HashSet<>(context.getCtxVars())); // add other elements in context (except ghosts) instanceVars.addAll(context.getCtxInstanceVars()); @@ -84,8 +84,8 @@ public String getScopePosition(CtElement element) { pos.getEndColumn()); } - public Map>> getVars() { - return vars; + public Map>> getFileScopeVars() { + return fileScopeVars; } public Set getInstanceVars() {