allowed support for verifying refinements declared in a separate package

Author: rodrigomilisse

liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java

@@ -18,7 +18,7 @@ public static void main(String[] args) {
         // In eclipse only needed this:"../liquidjava-example/src/main/java/"
         // In VSCode needs:
         // "../liquidjava/liquidjava-umbrella/liquidjava-example/src/main/java/liquidjava/test/project";
-        
+
         if (args.length == 0) {
             System.out.println("No input files or directories provided");
             System.out.println("\nUsage: ./liquidjava <...paths>");

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -551,24 +551,21 @@ private static String addInstanceWithState(TypeChecker tc, String superName, Str
                 prevInstance.getRefinement(), invocation);
         // vi2.setState(transitionedState);
         vi2.setRefinement(transitionedState);
-        RefinedVariable rv = superName != null ? tc.getContext().getVariableByName(superName) : null;
-        if (rv != null) {
-            // propagate supertypes from the refined variable
-            for (CtTypeReference<?> t : rv.getSuperTypes())
+        Context ctx = tc.getContext();
+        if (ctx.hasVariable(superName)) {
+            RefinedVariable rv = ctx.getVariableByName(superName);
+            for (CtTypeReference<?> t : rv.getSuperTypes()) {
                 vi2.addSuperType(t);
-        } else {
-            // propagate supertypes from the previous instance
-            for (CtTypeReference<?> t : prevInstance.getSuperTypes())
-                vi2.addSuperType(t);
-        }
+            }
 
-        // if the variable is a parent (not a VariableInstance) we need to check that
-        // this refinement
-        // is a subtype of the variable's main refinement
-        if (rv instanceof Variable) {
-            Predicate superC = rv.getMainRefinement().substituteVariable(rv.getName(), vi2.getName());
-            tc.checkSMT(superC, invocation);
-            tc.getContext().addRefinementInstanceToVariable(superName, name2);
+            // if the variable is a parent (not a VariableInstance) we need to check that
+            // this refinement
+            // is a subtype of the variable's main refinement
+            if (rv instanceof Variable) {
+                Predicate superC = rv.getMainRefinement().substituteVariable(rv.getName(), vi2.getName());
+                tc.checkSMT(superC, invocation);
+                tc.getContext().addRefinementInstanceToVariable(superName, name2);
+            }
         }
 
         invocation.putMetadata(tc.TARGET_KEY, vi2);