allowed support for verifying refinements declared in a separate package

Author: rodrigomilisse

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

@@ -57,11 +57,12 @@ public static ErrorEmitter launch(String... files) {
 
         try {
             // To only search the last package - less time spent
-            CtPackage v = factory.Package().getAll().stream().reduce((first, second) -> second).orElse(null);
-            if (v != null)
-                processingManager.process(v);
+            // CtPackage v = factory.Package().getAll().stream().reduce((first, second) ->
+            // second).orElse(null);
+            // if (v != null)
+            // processingManager.process(v);
             // To search all previous packages
-            // processingManager.process(factory.Package().getRootPackage());
+            processingManager.process(factory.Package().getRootPackage());
         } catch (Exception e) {
             e.printStackTrace();
             throw e;

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

@@ -528,18 +528,21 @@ private static String addInstanceWithState(TypeChecker tc, String superName, Str
                 prevInstance.getRefinement(), invocation);
         // vi2.setState(transitionedState);
         vi2.setRefinement(transitionedState);
-        RefinedVariable rv = tc.getContext().getVariableByName(superName);
-        for (CtTypeReference<?> t : rv.getSuperTypes()) {
-            vi2.addSuperType(t);
-        }
+        Context ctx = tc.getContext();
+        if (ctx.hasVariable(superName)) {
+            RefinedVariable rv = ctx.getVariableByName(superName);
+            for (CtTypeReference<?> t : rv.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);