Unwindset parsing: warn when label-based identifier is ambiguous

There are multiple possible loops matching a label-based identifier when
all loop heads are on the same line. Warn when this case is detected
instead of silently picking the inner loop, and also pick the outermost
loop instead.

Author: tautschnig

regression/cbmc/unwindset2/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  // clang-format off
+for_loop: for(int i=0; i<5; ++i) { while(i<5) ++i; }
+  // clang-format on
+  return 0;
+}

regression/cbmc/unwindset2/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--unwindset main.for_loop:2 --unwinding-assertions
+^loop identifier main.for_loop provided with unwindset is ambiguous$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/goto-instrument/unwindset.cpp

@@ -134,8 +134,14 @@ void unwindsett::parse_unwindset_one_loop(
             location.has_value() && instruction.is_backwards_goto() &&
             instruction.source_location() == *location)
           {
+            if(nr.has_value())
+            {
+              messaget log{message_handler};
+              log.warning()
+                << "loop identifier " << id
+                << " provided with unwindset is ambiguous" << messaget::eom;
+            }
             nr = instruction.loop_number;
-            break;
           }
         }
         if(!nr.has_value())