Update to EISOP 3.39-eisop1 from 3.34-eisop1 (#130)

opprop · Apr 7, 2024 · 0139154 · 0139154
1 parent 6e5b06d
commit 0139154
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 13 deletions.
diff --git a/src/ontology/OntologyAnnotatedTypeFactory.java b/src/ontology/OntologyAnnotatedTypeFactory.java
@@ -53,12 +53,14 @@ private final class OntologyQualifierHierarchy extends ElementQualifierHierarchy
         public OntologyQualifierHierarchy() {
             super(
                     OntologyAnnotatedTypeFactory.this.getSupportedTypeQualifiers(),
-                    OntologyAnnotatedTypeFactory.this.elements);
+                    OntologyAnnotatedTypeFactory.this.elements,
+                    OntologyAnnotatedTypeFactory.this);
             this.ONTOLOGY_KIND = getQualifierKind(OntologyUtils.ONTOLOGY);
         }
 
         @Override
-        public boolean isSubtype(AnnotationMirror subQualifier, AnnotationMirror superQualifier) {
+        public boolean isSubtypeQualifiers(
+                AnnotationMirror subQualifier, AnnotationMirror superQualifier) {
             if (getQualifierKind(subQualifier) != ONTOLOGY_KIND
                     || getQualifierKind(superQualifier) != ONTOLOGY_KIND) {
                 throw new BugInCF(
@@ -83,7 +85,7 @@ public boolean isSubtype(AnnotationMirror subQualifier, AnnotationMirror superQu
         }
 
         @Override
-        public @Nullable AnnotationMirror leastUpperBound(
+        public @Nullable AnnotationMirror leastUpperBoundQualifiers(
                 AnnotationMirror a1, AnnotationMirror a2) {
             if (getQualifierKind(a1) != ONTOLOGY_KIND || getQualifierKind(a2) != ONTOLOGY_KIND) {
                 throw new BugInCF("unexpected annotation mirrors: %s, %s", a1, a2);
@@ -99,7 +101,7 @@ public boolean isSubtype(AnnotationMirror subQualifier, AnnotationMirror superQu
         }
 
         @Override
-        public @Nullable AnnotationMirror greatestLowerBound(
+        public @Nullable AnnotationMirror greatestLowerBoundQualifiers(
                 AnnotationMirror a1, AnnotationMirror a2) {
             if (getQualifierKind(a1) != ONTOLOGY_KIND || getQualifierKind(a2) != ONTOLOGY_KIND) {
                 throw new BugInCF("unexpected annotation mirrors: %s, %s", a1, a2);

diff --git a/src/ontology/OntologyTypeValidator.java b/src/ontology/OntologyTypeValidator.java
@@ -14,7 +14,6 @@
 import org.checkerframework.framework.source.DiagMessage;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
-import org.checkerframework.framework.type.QualifierHierarchy;
 
 /**
  * This class checks the well-formedness of ontology values used inside an {@link Ontology}
@@ -30,10 +29,8 @@ public OntologyTypeValidator(
     }
 
     @Override
-    protected List<DiagMessage> isTopLevelValidType(
-            QualifierHierarchy qualifierHierarchy, AnnotatedTypeMirror type) {
-        List<DiagMessage> errorMsgs =
-                new ArrayList<>(super.isTopLevelValidType(qualifierHierarchy, type));
+    protected List<DiagMessage> isTopLevelValidType(AnnotatedTypeMirror type) {
+        List<DiagMessage> errorMsgs = new ArrayList<>(super.isTopLevelValidType(type));
 
         AnnotationMirror am = type.getAnnotation(Ontology.class);
         if (am != null) {

diff --git a/src/ontology/util/OntologyStatisticUtil.java b/src/ontology/util/OntologyStatisticUtil.java
@@ -223,7 +223,7 @@ public static void verifySolution(
                 continue;
             }
 
-            if (!qualifierHierarchy.isSubtype(subtype, supertype)) {
+            if (!qualifierHierarchy.isSubtypeQualifiersOnly(subtype, supertype)) {
                 ViolatedConsDiagnostic consDiagRes =
                         new ViolatedConsDiagnostic(sConstraint, subtype, supertype);
 

diff --git a/tests/ontology/OntologyTest.java b/tests/ontology/OntologyTest.java
@@ -6,8 +6,8 @@
 import java.util.List;
 import ontology.solvers.backend.OntologySolverEngine;
 import org.checkerframework.framework.test.TestUtilities;
-import org.checkerframework.javacutil.Pair;
 import org.junit.runners.Parameterized.Parameters;
+import org.plumelib.util.IPair;
 
 public class OntologyTest extends CFInferenceTest {
 
@@ -27,11 +27,11 @@ public boolean useHacks() {
     }
 
     @Override
-    public Pair<String, List<String>> getSolverNameAndOptions() {
+    public IPair<String, List<String>> getSolverNameAndOptions() {
         final String solverName = OntologySolverEngine.class.getCanonicalName();
         List<String> solverOptions = new ArrayList<>();
         solverOptions.add("solver=Z3");
-        return Pair.<String, List<String>>of(solverName, solverOptions);
+        return IPair.<String, List<String>>of(solverName, solverOptions);
     }
 
     @Parameters