Proof Management: Ignore internal contracts when calculating dependency state (fixes #3745)

keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/DependencyChecker.java

@@ -5,6 +5,9 @@
 
 import java.util.HashSet;
 import java.util.Set;
+import java.util.stream.Collectors;
+
+import de.uka.ilkd.key.speclang.Contract;
 
 import org.key_project.proofmanagement.check.dependency.DependencyGraph;
 import org.key_project.proofmanagement.check.dependency.DependencyNode;
@@ -122,8 +125,13 @@ private boolean hasUnprovenDependencies(DependencyGraph graph, CheckerData data)
                 if (!closed.contains(n)) {
                     CheckerData.ProofEntry entry = data.getProofEntryByContract(n.getContract());
                     if (entry != null) {
+                        Set<DependencyNode> deps = n.getDependencies().keySet();
+                        // filter out internal contracts (not in use-provided sources)
+                        Set<DependencyNode> userDeps = deps.stream().filter(
+                            d -> !MissingProofsChecker.isInternalContract(d.getContract(), data))
+                                .collect(Collectors.toSet());
                         if (entry.proofState == CheckerData.ProofState.CLOSED
-                                && closed.containsAll(n.getDependencies().keySet())) {
+                                && closed.containsAll(userDeps)) {
                             closed.add(n);
 
                             // update status in data object
@@ -149,10 +157,18 @@ private boolean hasUnprovenDependencies(DependencyGraph graph, CheckerData data)
         for (CheckerData.ProofEntry entry : data.getProofEntries()) {
             if (entry.dependencyState == CheckerData.DependencyState.UNKNOWN
                     && entry.replayState == CheckerData.ReplayState.SUCCESS) {
-                entry.dependencyState = CheckerData.DependencyState.UNPROVEN_DEP;
-                data.print(LogLevel.WARNING, "Unproven dependencies found for proof "
-                    + entry.proof.name());
-                hasUnprovenDeps = true;
+                Contract c = entry.contract;
+
+                if (MissingProofsChecker.isInternalContract(c, data)) {
+                    // unproven internal dependencies only result in a warning
+                    data.print(LogLevel.INFO, "Unproven internal dependencies found for proof "
+                        + entry.proof.name());
+                } else {
+                    entry.dependencyState = CheckerData.DependencyState.UNPROVEN_DEP;
+                    data.print(LogLevel.WARNING, "Unproven dependencies found for proof "
+                        + entry.proof.name());
+                    hasUnprovenDeps = true;
+                }
             }
         }
 

keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/MissingProofsChecker.java

@@ -100,23 +100,36 @@ private static void reportContractsWithoutProof(Set<Contract> contracts, Checker
             // Only contracts defined in files inside src directory of bundle are
             // considered. For other contracts (e.g. from bootclasspath) a message is
             // printed if loglevel is low enough.
-            Type type = c.getKJT().getJavaType();
-            if (type instanceof TypeDeclaration td) {
-                PositionInfo positionInfo = td.getPositionInfo();
-                URI uri = positionInfo.getURI().orElseThrow().normalize();
-                URI srcURI = data.getPbh().getPath("src").toAbsolutePath().normalize().toUri();
-
-
-                // ignore contracts from files not in src path (e.g. from bootclasspath)
-                // (this check works independent from number of slashes in URIs)
-                if (srcURI.relativize(uri).isAbsolute()) {
-                    data.addContractWithoutProof(c, true);
-                    data.print(LogLevel.DEBUG, "Ignoring internal contract " + c.getName());
-                    continue;
-                }
+            boolean internal = isInternalContract(c, data);
+            data.addContractWithoutProof(c, internal);
+            if (internal) {
+                data.print(LogLevel.INFO, "Ignoring internal contract " + c.getName());
+            } else {
+                data.print(LogLevel.WARNING, "No proof found for contract " + c.getName());
             }
-            data.addContractWithoutProof(c, false);
-            data.print(LogLevel.WARNING, "No proof found for contract " + c.getName());
         }
     }
+
+    /**
+     * This method checks if the given contract is an internal contract (i.e., it is not in the
+     * user-provided sources).
+     *
+     * @param c the contract to check
+     * @param data the CheckerData used as a basis
+     * @return true iff the contract is internal
+     */
+    public static boolean isInternalContract(Contract c, CheckerData data) {
+        Type type = c.getKJT().getJavaType();
+        if (type instanceof TypeDeclaration td) {
+            PositionInfo positionInfo = td.getPositionInfo();
+            URI uri = positionInfo.getURI().orElseThrow().normalize();
+            URI srcURI = data.getPbh().getPath("src").toAbsolutePath().normalize().toUri();
+
+            // ignore contracts from files not in src path (e.g. from bootclasspath)
+            // (this check works independent of number of slashes in URIs)
+            return srcURI.relativize(uri).isAbsolute();
+        }
+        // strange case: not sure what happened here ...
+        return false;
+    }
 }