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

We previously generated an assertion without setting either comments or
the property class. Make sure verification reports allow the user to
understand what the failing/succeeding assertion is about.

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);
     }