Fixed bug (class cast exception) in ProgVarReplacer

Drodt · Jan 10, 2025 · 4a12eb5 · 4a12eb5
1 parent cfc0e49
commit 4a12eb5
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 24 deletions.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java
@@ -33,13 +33,11 @@ public final class ProgVarReplacer {
      */
     private final Map<LocationVariable, LocationVariable> map;
 
-
     /**
      * The services object
      */
     private final Services services;
 
-
     /**
      * creates a ProgVarReplacer that replaces program variables as specified by the map parameter
      */
@@ -105,24 +103,30 @@ public SVInstantiations replace(SVInstantiations insts) {
             InstantiationEntry<?> ie = e.value();
             Object inst = ie.getInstantiation();
 
-            if (inst instanceof ContextStatementBlockInstantiation cie) {
-                ProgramElement pe = (ProgramElement) inst;
-                ProgramElement newPe = replace(pe);
+            if (inst instanceof Term t) {
+                final Term newT = replace(t);
+                if (newT != t) {
+                    result = result.replace(sv, newT, services);
+                }
+            } else if (inst instanceof ContextStatementBlockInstantiation cie) {
+                final ProgramElement pe = cie.program();
+                final ProgramElement newPe = replace(pe);
                 if (newPe != pe) {
-                    result = result.replace(cie.prefix(), cie.suffix(),
-                        cie.activeStatementContext(), newPe, services);
+                    result = result.replace(cie.prefix(), cie.suffix(), cie.activeStatementContext(), newPe, services);
                 }
-            } else if (ie instanceof org.key_project.logic.op.Operator) {
+            } else if (inst instanceof Operator) {
                 /* nothing to be done (currently) */
-            } else if (ie instanceof ProgramElement pe) {
-                ProgramElement newPe = replace(pe);
+            } else if (inst instanceof ProgramElement pe) {
+                final ProgramElement newPe = replace(pe);
                 if (newPe != pe) {
                     result = result.replace(sv, newPe, services);
                 }
-            } else if (ie instanceof ListInstantiation) {
-                @SuppressWarnings("unchecked")
-                ImmutableArray<ProgramElement> a = (ImmutableArray<ProgramElement>) inst;
-                int size = a.size();
+            } else if (ie instanceof ListInstantiation list) {
+                if (list.getType() != ProgramElement.class) {
+                    throw new RuntimeException("Unexpected list instantiation: " + ie);
+                }
+                final ImmutableArray<ProgramElement> a = (ImmutableArray<ProgramElement>) inst;
+                final int size = a.size();
                 ProgramElement[] array = new ProgramElement[size];
 
                 boolean changedSomething = false;
@@ -137,20 +141,14 @@ public SVInstantiations replace(SVInstantiations insts) {
                 if (changedSomething) {
                     result = result.replace(sv, new ImmutableArray<>(array), services);
                 }
-            } else if (inst instanceof Term t) {
-                final Term newT = replace(t);
-                if (newT != t) {
-                    result = result.replace(sv, newT, services);
-                }
-            } else {
+            }  else {
                 assert false : "unexpected subtype of InstantiationEntry<?>";
             }
         }
 
         return result;
     }
 
-
     /**
      * replaces in a sequent
      */
@@ -193,7 +191,6 @@ public SequentFormula replace(SequentFormula cf) {
         return result;
     }
 
-
     private Term replaceProgramVariable(Term t) {
         final ProgramVariable pv = (ProgramVariable) t.op();
         ProgramVariable o = map.get(pv);
@@ -203,7 +200,6 @@ private Term replaceProgramVariable(Term t) {
         return t;
     }
 
-
     private Term standardReplace(Term t) {
         Term result = t;
 
@@ -244,7 +240,6 @@ private Term standardReplace(Term t) {
         return result;
     }
 
-
     /**
      * replaces in a term
      */

diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/ListInstantiation.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/ListInstantiation.java
@@ -24,6 +24,12 @@ public ListInstantiation(ImmutableArray<T> pes, Class<T> type) {
         this.type = type;
     }
 
+    /** {@inheritDoc} */
+    @Override
+    public ImmutableArray<T> getInstantiation() {
+        return super.getInstantiation();
+    }
+
     /**
      * returns the element type of the contained instantiations
      */