Add Methods to Context History

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/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);