gistfile1.diff

commit 267746f2542b87447abd2b20f4fc3a658bd41a2a
Author: George Karpenkov <george@metaworld.ru>
Date:   Mon Sep 29 21:24:20 2014 +0200

    New interface for CompositeCPA, for easier
    strengthening.

diff --git a/src/org/sosy_lab/cpachecker/core/interfaces/ICompositeTransferRelation.java b/src/org/sosy_lab/cpachecker/core/interfaces/ICompositeTransferRelation.java
new file mode 100644
index 0000000..48d4fda
--- /dev/null
+++ b/src/org/sosy_lab/cpachecker/core/interfaces/ICompositeTransferRelation.java
@@ -0,0 +1,14 @@
+package org.sosy_lab.cpachecker.core.interfaces;
+
+import java.util.Collection;
+
+import org.sosy_lab.cpachecker.cfa.model.CFAEdge;
+import org.sosy_lab.cpachecker.exceptions.CPATransferException;
+
+public interface ICompositeTransferRelation extends TransferRelation {
+
+  public Collection<? extends AbstractState> getAbstractSuccessors(
+      Collection<AbstractState> otherStates,
+      AbstractState state, Precision precision, CFAEdge cfaEdge)
+      throws CPATransferException, InterruptedException;
+}
diff --git a/src/org/sosy_lab/cpachecker/cpa/composite/CompositeTransferRelation.java b/src/org/sosy_lab/cpachecker/cpa/composite/CompositeTransferRelation.java
index 6874d49..4ba47a6 100644
--- a/src/org/sosy_lab/cpachecker/cpa/composite/CompositeTransferRelation.java
+++ b/src/org/sosy_lab/cpachecker/cpa/composite/CompositeTransferRelation.java
@@ -30,6 +30,7 @@ import java.util.ArrayList;
 import java.util.Collection;
 import java.util.Collections;
 import java.util.HashSet;
+import java.util.LinkedList;
 import java.util.List;
 import java.util.Set;
 
@@ -37,6 +38,7 @@ import org.sosy_lab.cpachecker.cfa.model.CFAEdge;
 import org.sosy_lab.cpachecker.core.interfaces.AbstractState;
 import org.sosy_lab.cpachecker.core.interfaces.AbstractStateWithLocation;
 import org.sosy_lab.cpachecker.core.interfaces.ConfigurableProgramAnalysis;
+import org.sosy_lab.cpachecker.core.interfaces.ICompositeTransferRelation;
 import org.sosy_lab.cpachecker.core.interfaces.Precision;
 import org.sosy_lab.cpachecker.core.interfaces.TransferRelation;
 import org.sosy_lab.cpachecker.core.interfaces.pcc.ProofChecker;
@@ -109,12 +111,22 @@ public class CompositeTransferRelation implements TransferRelation {
     checkArgument(componentElements.size() == size, "State with wrong number of component states given");
     List<Collection<? extends AbstractState>> allComponentsSuccessors = new ArrayList<>(size);
 
+    Collection<AbstractState> tempSuccessors = new LinkedList<>();
+
     for (int i = 0; i < size; i++) {
       TransferRelation lCurrentTransfer = transferRelations.get(i);
       AbstractState lCurrentElement = componentElements.get(i);
       Precision lCurrentPrecision = compositePrecision.get(i);
 
-      Collection<? extends AbstractState> componentSuccessors = lCurrentTransfer.getAbstractSuccessors(lCurrentElement, lCurrentPrecision, cfaEdge);
+      Collection<? extends AbstractState> componentSuccessors;
+
+      if (lCurrentTransfer instanceof ICompositeTransferRelation) {
+        // TODO: hack =(
+        componentSuccessors = ((ICompositeTransferRelation)lCurrentTransfer).getAbstractSuccessors(
+            tempSuccessors, lCurrentElement, lCurrentPrecision, cfaEdge);
+      } else {
+        componentSuccessors = lCurrentTransfer.getAbstractSuccessors(lCurrentElement, lCurrentPrecision, cfaEdge);
+      }
       resultCount *= componentSuccessors.size();
 
       if (resultCount == 0) {
@@ -123,6 +135,7 @@ public class CompositeTransferRelation implements TransferRelation {
       }
 
       allComponentsSuccessors.add(componentSuccessors);
+      tempSuccessors.addAll(componentSuccessors);
     }
 
     // create cartesian product of all elements we got