Read a state value against the sets of the argument's subtypes too

liquidjava-example/src/main/java/testSuite/classes/state_value_set_of_subtype_correct/CloseFrame.java

@@ -0,0 +1,11 @@
+package testSuite.classes.state_value_set_of_subtype_correct;
+
+import javax.swing.JFrame;
+
+public class CloseFrame {
+    static void close() {
+        JFrame frame = new JFrame();
+        if (frame.isDisplayable())
+            frame.dispose();
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/state_value_set_of_subtype_correct/ComponentRefinements.java

@@ -0,0 +1,11 @@
+package testSuite.classes.state_value_set_of_subtype_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+
+// the set is declared on Window, a subclass of Component
+@ExternalRefinementsFor("java.awt.Component")
+public interface ComponentRefinements {
+    @Refinement("_ ? display(this) == displayable : display(this) == notDisplayable")
+    boolean isDisplayable();
+}

liquidjava-example/src/main/java/testSuite/classes/state_value_set_of_subtype_correct/JFrameRefinements.java

@@ -0,0 +1,10 @@
+package testSuite.classes.state_value_set_of_subtype_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("javax.swing.JFrame")
+public interface JFrameRefinements {
+    @StateRefinement(to = "display(this) == notDisplayable")
+    void JFrame();
+}

liquidjava-example/src/main/java/testSuite/classes/state_value_set_of_subtype_correct/WindowRefinements.java

@@ -0,0 +1,12 @@
+package testSuite.classes.state_value_set_of_subtype_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("java.awt.Window")
+@StateSet(name = "display", value = {"notDisplayable", "displayable"})
+public interface WindowRefinements {
+    @StateRefinement(from = "display(this) == displayable", to = "display(this) == notDisplayable")
+    void dispose();
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -398,7 +398,7 @@ protected void getGhostFunction(String value, CtElement element, SourcePosition
      */
     public Predicate readStateValues(Predicate p, CtElement element, SourcePosition position) throws LJError {
         StateValues values = new StateValues(context.getGhostStates(), name -> isVariableIn(element, name),
-                argument -> typeIn(element, argument).map(type -> set -> isOfType(type, set.getPrefix())));
+                argument -> typeIn(element, argument).map(type -> set -> isRelatedTo(type, set.getPrefix())));
         try {
             return new Predicate(values.toShorthand(p.getExpression()));
         } catch (LJError e) {
@@ -449,13 +449,17 @@ private StateValues aliasStateValues(AliasDTO alias, String klass, String path)
                 return Optional.empty();
             CtTypeReference<?> type = AliasWrapper.parameterType(alias.getVarTypes().get(parameter), factory, klass,
                     path);
-            return Optional.of(set -> isOfType(type, set.getPrefix()));
+            return Optional.of(set -> isRelatedTo(type, set.getPrefix()));
         });
     }
 
-    /** Whether {@code type} is the class {@code className} or one of its subtypes */
-    private boolean isOfType(CtTypeReference<?> type, String className) {
-        return type.getQualifiedName().equals(className) || type.isSubtypeOf(factory.Type().createReference(className));
+    /**
+     * Whether a value of {@code type} can be of the class {@code className}: it is that class, one of its subtypes or
+     * one of its supertypes
+     */
+    private boolean isRelatedTo(CtTypeReference<?> type, String className) {
+        CtTypeReference<?> klass = factory.Type().createReference(className);
+        return type.getQualifiedName().equals(className) || type.isSubtypeOf(klass) || klass.isSubtypeOf(type);
     }
 
     protected void handleAlias(String ref, CtElement element, SourcePosition position) throws LJError {