From a680f6f435cf499fc646185aeb8dd47c4aff14a1 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 24 Sep 2025 14:54:03 +0100 Subject: [PATCH] Analyze All Packages In Directory --- .../java/liquidjava/api/CommandLineLauncher.java | 10 ++++------ .../object_checkers/AuxStateHandler.java | 12 +++++++++--- 2 files changed, 13 insertions(+), 9 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 82c3f024..ea1fecb7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/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; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index f21329aa..13435684 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/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