Add Methods to Context History

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java

@@ -17,13 +17,15 @@ public class ContextHistory {
     private Set<GhostState> ghosts;
     private Set<AliasWrapper> aliases;
     private Set<RefinedVariable> globalVars;
+    private Set<RefinedFunction> methods;
 
     private ContextHistory() {
         fileScopes = new HashMap<>();
         localVars = new HashSet<>();
         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<AliasWrapper> getAliases() {
         return aliases;
     }
 
+    public Set<RefinedFunction> getMethods() {
+        return methods;
+    }
+
     public Map<String, Set<String>> getFileScopes() {
         return fileScopes;
     }

liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java

@@ -12,6 +12,7 @@ public class RefinedFunction extends Refined {
     private String targetClass;
     private List<ObjectState> 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);
     }

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 <R> void getMethodRefinements(CtMethod<R> 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 <R> void getMethodRefinements(CtMethod<R> 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()));