Fix line-number output in document-properties-*

The `line_no` variable was never used in producing the output, even
though it was written to (and in parts also used in an expression
without having an effect, which tripped up the compiler with newer
standards versions).

Author: tautschnig

regression/goto-instrument/document-properties-basic/html.desc

@@ -3,7 +3,7 @@ main.c
 --document-properties-html
 ^EXIT=0$
 ^SIGNAL=0$
-^<em>  assert\(1 == 1\);<\/em>$
+^\s*\d+&nbsp;&nbsp;<em>  assert\(1 == 1\);<\/em>$
 --
 ^warning: ignoring
 --

src/goto-instrument/document_properties.cpp

@@ -225,6 +225,11 @@ document_propertiest::get_code(const source_locationt &source_location)
 
   // build dest
 
+  std::size_t max_line_number_width = 0;
+  if(!lines.empty())
+  {
+    max_line_number_width = std::to_string(lines.back().line_number).size();
+  }
   for(std::list<linet>::iterator it=lines.begin();
       it!=lines.end(); it++)
   {
@@ -235,10 +240,10 @@ document_propertiest::get_code(const source_locationt &source_location)
     switch(format)
     {
     case LATEX:
-      while(line_no.size()<4)
+      while(line_no.size() < max_line_number_width)
         line_no=" "+line_no;
 
-      line_no+"  ";
+      line_no += "  ";
 
       tmp+=escape_latex(it->text, true);
 
@@ -248,10 +253,10 @@ document_propertiest::get_code(const source_locationt &source_location)
       break;
 
     case HTML:
-      while(line_no.size()<4)
+      while(line_no.size() < max_line_number_width)
         line_no="&nbsp;"+line_no;
 
-      line_no+"&nbsp;&nbsp;";
+      line_no += "&nbsp;&nbsp;";
 
       tmp+=escape_html(it->text);
 
@@ -261,7 +266,7 @@ document_propertiest::get_code(const source_locationt &source_location)
       break;
     }
 
-    dest+=tmp+"\n";
+    dest += line_no + tmp + "\n";
   }
 
   return dest;