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

We previously generated an assertion without setting either comments or
property_ids. 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,6 +1,7 @@
 CORE
 main.c
 --unwind 10 --unwinding-assertions
+^\[main.unwind.0\] line 5 unwinding assertion loop 0: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

src/goto-instrument/unwind.cpp

@@ -153,8 +153,15 @@ 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_property_id(
+        id2string(function_id) + ".unwind." + loop_number);
+      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);
     }