Merge pull request #7262 from tautschnig/feature/goto-instrument-unwind-id

goto-instrument --unwind: identify loop unwinding assertions as such

Author: tautschnig

regression/goto-instrument/unwind-assert1/test.desc

@@ -1,8 +1,10 @@
 CORE
 main.c
 --unwind 10 --unwinding-assertions
+^\[main.unwind.1\] line 5 unwinding assertion loop 0: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+^\[main.\d+\] line 5 assertion: SUCCESS$

src/goto-instrument/unwind.cpp

@@ -153,8 +153,13 @@ void goto_unwindt::unwind(
       unwind_strategy == unwind_strategyt::ASSERT_ASSUME ||
       unwind_strategy == unwind_strategyt::ASSERT_PARTIAL)
     {
+      const std::string loop_number = std::to_string(t->loop_number);
+      source_locationt source_location_annotated = loop_head->source_location();
+      source_location_annotated.set_property_class("unwind");
+      source_location_annotated.set_comment(
+        "unwinding assertion loop " + loop_number);
       goto_programt::targett assertion = rest_program.add(
-        goto_programt::make_assertion(exit_cond, loop_head->source_location()));
+        goto_programt::make_assertion(exit_cond, source_location_annotated));
       unwind_log.insert(assertion, loop_head->location_number);
     }