diff --git a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java index 6ab937113e8..9ec5703b082 100644 --- a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java +++ b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java @@ -1118,14 +1118,7 @@ private BoogieIcfgLocation getLocNodeForLabel(final DebugIdentifier labelId, fin mLogger.debug("LocNode for " + labelId + " already" + " constructed, namely: " + locNode); } if (st instanceof Label && locNode.getDebugIdentifier() == labelId) { - loc.annotate(locNode); - if (lea != null && lea.getLoopEntryType() == LoopEntryType.WHILE) { - if (mLogger.isDebugEnabled()) { - mLogger.debug("LocNode does not have to Location of the while loop" + st.getLocation()); - } - mIcfg.getLoopLocations().add(locNode); - } } ModelUtils.copyAnnotations(st, locNode); return locNode; @@ -1136,9 +1129,6 @@ private BoogieIcfgLocation getLocNodeForLabel(final DebugIdentifier labelId, fin if (mLogger.isDebugEnabled()) { mLogger.debug("LocNode for " + labelId + " has not" + " existed yet. Constructed it"); } - if (lea != null && lea.getLoopEntryType() == LoopEntryType.WHILE) { - mIcfg.getLoopLocations().add(locNode); - } return locNode; } @@ -1150,7 +1140,7 @@ private void processLabel(final Label st) { } final StringDebugIdentifier tmpLabelIdentifier = new StringDebugIdentifier(labelName); if (mCurrent instanceof BoogieIcfgLocation) { - // from now on this label is represented by mcurrent + // from now on this label is represented by mCurrent final BoogieIcfgLocation oldNodeForLabel = mLabel2LocNodes.get(tmpLabelIdentifier); if (oldNodeForLabel != null) { @@ -1161,9 +1151,9 @@ private void processLabel(final Label st) { mLastLabelName = tmpLabelIdentifier; // mlocSuffix = 0; - // is there already a LocNode that represents this - // label? (This can be the case if this label was destination - // of a goto statement) If not construct the LocNode. + // Is there already a LocNode that represents this label? + // (This can be the case if this label was destination of a goto statement.) + // If not construct the LocNode. // If yes, add the Location Object to the existing LocNode. final BoogieIcfgLocation locNode = getLocNodeForLabel(tmpLabelIdentifier, st); @@ -1173,6 +1163,13 @@ private void processLabel(final Label st) { } mCurrent = locNode; } + + // Mark the current location as loop location if necessary. + final LoopEntryAnnotation lea = LoopEntryAnnotation.getAnnotation(st); + if (lea != null && lea.getLoopEntryType() == LoopEntryType.WHILE) { + mLogger.debug("LocNode %s is marked as loop head (location: %s)", mCurrent, st.getLocation()); + mIcfg.getLoopLocations().add((BoogieIcfgLocation) mCurrent); + } } private void processAssuAssiHavoStatement(final Statement st, final Origin origin) {