Merge pull request #677 from ultimate-pa/wip/mh/atomicblockinfo

Let AtomicBlockInfo use more precise types
ultimate-pa · Aug 31, 2024 · f49a868 · f49a868
2 parents 1e7ed35 + a9f6b24
commit f49a868
Show file tree

Hide file tree

Showing 2 changed files with 32 additions and 32 deletions.
diff --git a/...e/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/AtomicBlockInfo.java b/...e/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/AtomicBlockInfo.java
@@ -31,9 +31,9 @@
 import java.util.function.IntPredicate;
 
 import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.ModernAnnotations;
-import de.uni_freiburg.informatik.ultimate.core.model.models.IElement;
 import de.uni_freiburg.informatik.ultimate.core.model.models.ModelUtils;
 import de.uni_freiburg.informatik.ultimate.core.model.models.annotation.IAnnotations;
+import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IIcfgTransition;
 
 /**
  * An annotation used to mark CFG edges that are the beginning or end of an atomic block, in the sense of SV-COMP's
@@ -82,36 +82,36 @@ public String toString() {
 	 *
 	 * Note that an edge can be the start of an atomic block or the end, but not both.
 	 *
-	 * @param element
-	 *            The element whose annotation is examined.
+	 * @param edge
+	 *            The edge whose annotation is examined.
 	 * @return true if there is an {@link AtomicBlockInfo} annotation that marks the beginning of an atomic block.
 	 */
-	public static boolean isStartOfAtomicBlock(final IElement element) {
-		return hasAnnotatedDelta(element, d -> d > 0);
+	public static boolean isStartOfAtomicBlock(final IIcfgTransition<?> edge) {
+		return hasAnnotatedDelta(edge, d -> d > 0);
 	}
 
 	/**
 	 * Determines if the given element (an edge) is annotated as end of an atomic block.
 	 *
 	 * Note that an edge can be the start of an atomic block or the end, but not both.
 	 *
-	 * @param element
-	 *            The element whose annotation is examined.
+	 * @param edge
+	 *            The edge whose annotation is examined.
 	 * @return true if there is an {@link AtomicBlockInfo} annotation that marks the end of an atomic block.
 	 */
-	public static boolean isEndOfAtomicBlock(final IElement element) {
-		return hasAnnotatedDelta(element, d -> d < 0);
+	public static boolean isEndOfAtomicBlock(final IIcfgTransition<?> edge) {
+		return hasAnnotatedDelta(edge, d -> d < 0);
 	}
 
 	/**
 	 * Determines if the given element (an edge) is annotated as the result of a complete atomic block composition.
 	 *
-	 * @param element
-	 *            The element whose annotation is examined.
+	 * @param edge
+	 *            The edge whose annotation is examined.
 	 * @return true if there is an {@link AtomicBlockInfo} annotation that marks a complete atomic block.
 	 */
-	public static boolean isCompleteAtomicBlock(final IElement element) {
-		return hasAnnotatedDelta(element, d -> d == 0);
+	public static boolean isCompleteAtomicBlock(final IIcfgTransition<?> edge) {
+		return hasAnnotatedDelta(edge, d -> d == 0);
 	}
 
 	/**
@@ -120,8 +120,8 @@ public static boolean isCompleteAtomicBlock(final IElement element) {
 	 * @param element
 	 *            The edge to be marked.
 	 */
-	public static void addBeginAnnotation(final IElement element) {
-		addAnnotation(element, START_DELTA);
+	public static void addBeginAnnotation(final IIcfgTransition<?> edge) {
+		addAnnotation(edge, START_DELTA);
 	}
 
 	/**
@@ -130,8 +130,8 @@ public static void addBeginAnnotation(final IElement element) {
 	 * @param element
 	 *            The edge to be marked.
 	 */
-	public static void addEndAnnotation(final IElement element) {
-		addAnnotation(element, END_DELTA);
+	public static void addEndAnnotation(final IIcfgTransition<?> edge) {
+		addAnnotation(edge, END_DELTA);
 	}
 
 	/**
@@ -140,34 +140,34 @@ public static void addEndAnnotation(final IElement element) {
 	 * @param element
 	 *            The edge to be marked.
 	 */
-	public static void addCompleteAnnotation(final IElement element) {
-		addAnnotation(element, 0);
+	public static void addCompleteAnnotation(final IIcfgTransition<?> edge) {
+		addAnnotation(edge, 0);
 	}
 
 	/**
 	 * Removes any {@link AtomicBlockInfo} annotation, if present.
 	 *
 	 * @param element
-	 *            The edge from which annotations shall be removed
+	 *            The edge from which annotations shall be removed.
 	 */
-	public static void removeAnnotation(final IElement element) {
-		element.getPayload().getAnnotations().remove(AtomicBlockInfo.class.getName());
+	public static void removeAnnotation(final IIcfgTransition<?> edge) {
+		edge.getPayload().getAnnotations().remove(AtomicBlockInfo.class.getName());
 	}
 
-	private static boolean hasAnnotatedDelta(final IElement element, final IntPredicate condition) {
-		final AtomicBlockInfo annotation = ModelUtils.getAnnotation(element, AtomicBlockInfo.class);
+	private static boolean hasAnnotatedDelta(final IIcfgTransition<?> edge, final IntPredicate condition) {
+		final AtomicBlockInfo annotation = ModelUtils.getAnnotation(edge, AtomicBlockInfo.class);
 		if (annotation != null) {
 			return condition.test(annotation.mDelta);
 		}
 		return false;
 	}
 
-	private static void addAnnotation(final IElement element, final int delta) {
-		final var previous = ModelUtils.getAnnotation(element, AtomicBlockInfo.class);
+	private static void addAnnotation(final IIcfgTransition<?> edge, final int delta) {
+		final var previous = ModelUtils.getAnnotation(edge, AtomicBlockInfo.class);
 		if (previous != null) {
 			throw new UnsupportedOperationException(
 					"Incompatible atomic block annotation: " + previous.mDelta + " and " + delta);
 		}
-		element.getPayload().getAnnotations().put(AtomicBlockInfo.class.getName(), new AtomicBlockInfo(delta));
+		edge.getPayload().getAnnotations().put(AtomicBlockInfo.class.getName(), new AtomicBlockInfo(delta));
 	}
 }
diff --git a/...src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java b/...src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java
@@ -1527,7 +1527,7 @@ private void beginAtomicBlock(final Statement st) {
 			assert mCurrent instanceof CodeBlock : "Start marker for atomic section must be an edge";
 
 			// mark current edge as start of atomic block
-			AtomicBlockInfo.addBeginAnnotation(mCurrent);
+			AtomicBlockInfo.addBeginAnnotation((IIcfgTransition<?>) mCurrent);
 		}
 
 		private void endAtomicBlock(final Statement st) {
@@ -1537,13 +1537,13 @@ private void endAtomicBlock(final Statement st) {
 			}
 			assert mCurrent instanceof CodeBlock : "End marker for atomic section must be an edge";
 
-			if (AtomicBlockInfo.isStartOfAtomicBlock(mCurrent)) {
+			if (AtomicBlockInfo.isStartOfAtomicBlock((IIcfgTransition<?>) mCurrent)) {
 				// if current edge is both start and end of an atomic block, it is already atomic -- nothing else to do
-				AtomicBlockInfo.removeAnnotation(mCurrent);
-				AtomicBlockInfo.addCompleteAnnotation(mCurrent);
+				AtomicBlockInfo.removeAnnotation((IIcfgTransition<?>) mCurrent);
+				AtomicBlockInfo.addCompleteAnnotation((IIcfgTransition<?>) mCurrent);
 			} else {
 				// mark current edge as end of atomic block
-				AtomicBlockInfo.addEndAnnotation(mCurrent);
+				AtomicBlockInfo.addEndAnnotation((IIcfgTransition<?>) mCurrent);
 			}
 
 			// ensure nothing is appended to current edge