Analyze All Packages In Directory

Author: rcosta358

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

@@ -53,12 +53,10 @@ public static ErrorEmitter launch(String file) {
         processingManager.addProcessor(processor);
 
         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);
-            // To search all previous packages
-            // processingManager.process(factory.Package().getRootPackage());
+            // analyze all packages
+            CtPackage root = factory.Package().getRootPackage();
+            if (root != null)
+                processingManager.process(root);
         } catch (Exception e) {
             e.printStackTrace();
             throw e;

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

@@ -528,9 +528,15 @@ 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);
+        RefinedVariable rv = superName != null ? tc.getContext().getVariableByName(superName) : null;
+        if (rv != null) {
+            // propagate supertypes from the refined variable
+            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