Merge pull request #6769 from tautschnig/feature/unwindset-warning

Unwindset parsing: warn when label-based identifier is ambiguous

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