Do not suppress loop head locations in the trace

In the trace, we only output the first location of a sequence
of same locations.
However, we don't want to suppress loop head locations because
they might come from different loop iterations. If we suppressed
them it would be impossible to know in which loop iteration
we are in.

Author: peterschrammel

src/goto-programs/xml_goto_trace.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening
 #include <util/symbol.h>
 #include <util/xml_irep.h>
 
+#include <algorithm>
 #include <langapi/language_util.h>
 #include <util/arith_tools.h>
 
@@ -237,12 +238,23 @@ void convert(
     case goto_trace_stept::typet::GOTO:
     case goto_trace_stept::typet::ASSUME:
     case goto_trace_stept::typet::NONE:
-      if(source_location!=previous_source_location)
+    {
+      // If this is just a source location then we output only the first
+      // location of a sequence of same locations.
+      // However, we don't want to suppress loop head locations because
+      // they might come from different loop iterations. If we suppressed
+      // them it would be impossible to know in which loop iteration
+      // we are in.
+      const bool is_loophead = std::any_of(
+        step.pc->incoming_edges.begin(),
+        step.pc->incoming_edges.end(),
+        [](goto_programt::targett t) { return t->is_backwards_goto(); });
+      if(source_location != previous_source_location || is_loophead)
       {
-        // just the source location
         if(!xml_location.name.empty())
         {
-          xmlt &xml_location_only=dest.new_element("location-only");
+          xmlt &xml_location_only =
+            dest.new_element(is_loophead ? "loop-head" : "location-only");
 
           xml_location_only.set_attribute_bool("hidden", step.hidden);
           xml_location_only.set_attribute(
@@ -253,6 +265,8 @@ void convert(
           xml_location_only.new_element().swap(xml_location);
         }
       }
+      break;
+    }
     }
 
     if(source_location.is_not_nil() && !source_location.get_file().empty())