fix determination of loop locations

Previously, the loop heads of loops immediately following
a procedure entry were not marked as loop locations. This
change fixes this, by pulling the code out of the method
getLocNodeForLabel into the caller method processLabel,
where it is also executed in case the mCurrent is already
a location (and not a statement).

getLocNodeForLabel is also called from processGotoStatement,
but it should be enough to mark the node as loop location once
(when the label is processed) rather than repeat this for every
goto statement to this label.

The commit also fixes the debug log message.

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) {