From f972150265beff86f2b1ae234c7e77c97b933fd3 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 26 Mar 2022 21:17:09 +0000
Subject: [PATCH] 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.
---
 regression/cbmc/unwindset2/main.c    | 7 +++++++
 regression/cbmc/unwindset2/test.desc | 9 +++++++++
 src/goto-instrument/unwindset.cpp    | 8 +++++++-
 3 files changed, 23 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/unwindset2/main.c
 create mode 100644 regression/cbmc/unwindset2/test.desc

diff --git a/regression/cbmc/unwindset2/main.c b/regression/cbmc/unwindset2/main.c
new file mode 100644
index 00000000000..ea4df05d664
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/unwindset2/test.desc b/regression/cbmc/unwindset2/test.desc
new file mode 100644
index 00000000000..e870637450c
--- /dev/null
+++ b/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
diff --git a/src/goto-instrument/unwindset.cpp b/src/goto-instrument/unwindset.cpp
index 430a4dea1e2..7b0168ccdd0 100644
--- a/src/goto-instrument/unwindset.cpp
+++ b/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())