#295, incremental changes

ultimate-pa · Jan 28, 2018 · 6c736d0 · 6c736d0
1 parent 06c19df
commit 6c736d0
Show file tree

Hide file tree

Showing 4 changed files with 74 additions and 5 deletions.
diff --git a/...er/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/IcfgTransitionTransformer.java b/...er/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/IcfgTransitionTransformer.java
@@ -165,6 +165,7 @@ protected IcfgEdge transform(final IcfgEdge oldTransition, final OUTLOC newSourc
 	private void log(final IcfgEdge oldTransition, final IcfgEdge newTransition) {
 		mLogger.debug("transformed oldTransition " + oldTransition);
 		mLogger.debug("\t  to : " + newTransition);
+		mLogger.debug("");
 	}
 
 

diff --git a/...ni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapSepIcfgTransformer.java b/...ni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapSepIcfgTransformer.java
@@ -418,11 +418,7 @@ void processSelect(final SelectInfo selectInfo, final IEqualityProvidingIntermed
 				mSelectInfoToDimensionToToSampleStoreIndexInfo.put(selectInfo, dim, nsii);
 				continue;
 			}
-//			} else if (mayEqualStoreIndexInfos.size() <= 1) {
-//				// nothing to do
-//				final StoreIndexInfo sample = mayEqualStoreIndexInfos.iterator().next();
-//				mSelectInfoToDimensionToToSampleStoreIndexInfo.put(selectInfo, i, sample);
-//			} else {
+
 			final StoreIndexInfo sample = mayEqualStoreIndexInfos.iterator().next();
 
 			mSelectInfoToDimensionToToSampleStoreIndexInfo.put(selectInfo, dim, sample);
@@ -495,6 +491,7 @@ public void finish() {
 			mSelectInfoToDimensionToLocationBlock.put(selectInfo, dim, locationBlock);
 			mLogger.debug("adding LocationBlock " + locationBlock);
 			mLogger.debug("\t at dimension " + dim + " for " + selectInfo);
+			mLogger.debug("\t write locations: " + locationBlock.getLocations());
 
 		}
 		mIsFinished = true;
@@ -508,6 +505,14 @@ public void finish() {
 						mArrayGroupToDimensionToStoreIndexInfoPartition.get(arrayGroup, dim).getAllElements().size());
 				mLogger.info("\t # location blocks :" +
 						mArrayGroupToDimensionToStoreIndexInfoPartition.get(arrayGroup, dim).getAllEquivalenceClasses().size());
+
+				mLogger.debug("\t location block contents:");
+				if (mLogger.isDebugEnabled()) {
+					for (final Set<StoreIndexInfo> eqc
+							: mArrayGroupToDimensionToStoreIndexInfoPartition.get(arrayGroup, dim).getAllEquivalenceClasses()) {
+						mLogger.debug("\t\t " + eqc);
+					}
+				}
 			}
 		}
 

diff --git a/...mer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/SelectInfo.java b/...mer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/SelectInfo.java
@@ -46,4 +46,44 @@ public ArrayIndex getIndex() {
 	public ArrayCellAccess getArrayCellAccess() {
 		return mArrayCellAccess;
 	}
+
+	@Override
+	public int hashCode() {
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((mArrayCellAccess == null) ? 0 : mArrayCellAccess.hashCode());
+		result = prime * result + ((mEdgeInfo == null) ? 0 : mEdgeInfo.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(final Object obj) {
+		if (this == obj) {
+			return true;
+		}
+		if (obj == null) {
+			return false;
+		}
+		if (getClass() != obj.getClass()) {
+			return false;
+		}
+		final SelectInfo other = (SelectInfo) obj;
+		if (mArrayCellAccess == null) {
+			if (other.mArrayCellAccess != null) {
+				return false;
+			}
+		} else if (!mArrayCellAccess.equals(other.mArrayCellAccess)) {
+			return false;
+		}
+		if (mEdgeInfo == null) {
+			if (other.mEdgeInfo != null) {
+				return false;
+			}
+		} else if (!mEdgeInfo.equals(other.mEdgeInfo)) {
+			return false;
+		}
+		return true;
+	}
+
+
 }
diff --git a/...src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/StoreIndexInfo.java b/...src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/StoreIndexInfo.java
@@ -199,4 +199,27 @@ public NoStoreIndexInfo() {
 		super(null, null);
 	}
 
+	@Override
+	public int hashCode() {
+		return 0;
+	}
+
+	@Override
+	public boolean equals(final Object obj) {
+		if (this == obj) {
+			return true;
+		}
+		if (obj == null) {
+			return false;
+		}
+		if (getClass() != obj.getClass()) {
+			return false;
+		}
+		return true;
+	}
+
+	@Override
+	public String toString() {
+		return "NoStoreIndexInfo";
+	}
 }