Add distances to property as variable in locst

Also fixes indentation and whitespace in the output function, and replaces unsigned with std::size_t, based on feedback from tautschn

Author: polgreen

src/path-symex/locs.cpp

@@ -86,19 +86,23 @@ void locst::output(std::ostream &out) const
 {
   irep_idt function;
 
-  for(unsigned l=0; l<loc_vector.size(); l++)
+  for(std::size_t l = 0; l < loc_vector.size(); l++)
   {
-    const loct &loc=loc_vector[l];
-    if(function!=loc.function)
+    const loct &loc = loc_vector[l];
+    if(function != loc.function)
     {
-      function=loc.function;
+      function = loc.function;
       out << "*** " << function << "\n";
     }
 
     out << "  L" << l << ": "
 //        << loc.target->type << " "
 //        << loc.target->location
-        << " " << as_string(ns, *loc.target) << "\n";
+        << " " << as_string(ns, *loc.target);
+    if(loc_vector[l].distance_to_property
+        != std::numeric_limits<std::size_t>::max())
+      out << " path length: " << loc_vector[l].distance_to_property;
+    out << "\n";
 
     if(!loc.branch_target.is_nil())
       out << "    T: " << loc.branch_target << "\n";

src/path-symex/locs.h

@@ -27,11 +27,12 @@ struct loct
     target(_target),
     function(_function)
   {
+    distance_to_property=std::numeric_limits<std::size_t>::max();
   }
 
   goto_programt::const_targett target;
   irep_idt function;
-
+  std::size_t distance_to_property;
   // we only support a single branch target
   loc_reft branch_target;
 };