Unwindset parsing: warn when label-based identifier is ambiguous

[tautschnig]

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.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Merging #6769 (f972150) into develop (dea6182) will increase coverage by 0.00%.
The diff coverage is 100.00%.

@@           Coverage Diff            @@
##           develop    #6769   +/-   ##
========================================
  Coverage    76.90%   76.90%           
========================================
  Files         1590     1590           
  Lines       183963   183970    +7     
========================================
+ Hits        141477   141484    +7     
  Misses       42486    42486           

Impacted Files	Coverage Δ
src/goto-instrument/unwindset.cpp	85.84% <100.00%> (+0.70%)	⬆️
src/goto-symex/goto_symex_state.cpp	91.71% <100.00%> (+0.04%)	⬆️

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update bb08494...f972150. Read the comment docs.