All if-then-else goto conversion instructions have a location

We must not produce goto-program instructions without location, even
when they are considered dummy instructions: those instructions may
subsequently be used to produce a source location, which was thus
missing when converting nested if-then-else statements.

Author: tautschnig

Diff for: regression/cbmc-cover/location3/main.c

@@ -0,0 +1,22 @@
+int main()
+{
+  int b, c;
+
+  if(b)
+  {
+    if(c)
+    {
+      c = 1;
+    }
+    else
+    {
+      c = 2;
+    }
+  }
+  else
+  {
+    b = 0;
+  }
+
+  return 1;
+}

Diff for: regression/cbmc-cover/location3/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.coverage.\d+\] file main.c line 9 function main block \d+ \(lines main.c:main:9,10\): SATISFIED$
+^\[main.coverage.\d+\] file main.c line 15 function main block \d+ \(lines main.c:main:15\): SATISFIED$
+^\*\* 7 of 7 covered \(100.0%\)
+--
+^warning: ignoring
+--
+All gotos must have a source location annotated.

Diff for: src/goto-programs/goto_clean_expr.cpp

@@ -284,7 +284,14 @@ void goto_convertt::clean_expr(
 
     // generate guard for argument side-effects
     generate_ifthenelse(
-      if_expr.cond(), tmp_true, tmp_false, source_location, dest, mode);
+      if_expr.cond(),
+      source_location,
+      tmp_true,
+      if_expr.true_case().source_location(),
+      tmp_false,
+      if_expr.false_case().source_location(),
+      dest,
+      mode);
 
     return;
   }

Diff for: src/goto-programs/goto_convert.cpp

@@ -1613,17 +1613,34 @@ void goto_convertt::convert_ifthenelse(
   // convert 'then'-branch
   goto_programt tmp_then;
   convert(code.then_case(), tmp_then, mode);
+  source_locationt then_end_location =
+    code.then_case().get_statement() == ID_block
+      ? to_code_block(code.then_case()).end_location()
+      : code.then_case().source_location();
 
   goto_programt tmp_else;
+  source_locationt else_end_location;
 
   if(has_else)
+  {
     convert(code.else_case(), tmp_else, mode);
+    else_end_location = code.else_case().get_statement() == ID_block
+                          ? to_code_block(code.else_case()).end_location()
+                          : code.else_case().source_location();
+  }
 
   exprt tmp_guard=code.cond();
   clean_expr(tmp_guard, dest, mode);
 
   generate_ifthenelse(
-    tmp_guard, tmp_then, tmp_else, source_location, dest, mode);
+    tmp_guard,
+    source_location,
+    tmp_then,
+    then_end_location,
+    tmp_else,
+    else_end_location,
+    dest,
+    mode);
 }
 
 void goto_convertt::collect_operands(
@@ -1655,9 +1672,11 @@ static inline bool is_size_one(const goto_programt &g)
 /// if(guard) true_case; else false_case;
 void goto_convertt::generate_ifthenelse(
   const exprt &guard,
+  const source_locationt &source_location,
   goto_programt &true_case,
+  const source_locationt &then_end_location,
   goto_programt &false_case,
-  const source_locationt &source_location,
+  const source_locationt &else_end_location,
   goto_programt &dest,
   const irep_idt &mode)
 {
@@ -1727,13 +1746,17 @@ void goto_convertt::generate_ifthenelse(
 
   // Flip around if no 'true' case code.
   if(is_empty(true_case))
+  {
     return generate_ifthenelse(
       boolean_negate(guard),
+      source_location,
       false_case,
+      else_end_location,
       true_case,
-      source_location,
+      then_end_location,
       dest,
       mode);
+  }
 
   bool has_else=!is_empty(false_case);
 
@@ -1753,14 +1776,13 @@ void goto_convertt::generate_ifthenelse(
 
   // do the x label
   goto_programt tmp_x;
-  goto_programt::targett x = tmp_x.add(goto_programt::make_incomplete_goto(
-    true_exprt(), true_case.instructions.back().source_location()));
+  goto_programt::targett x = tmp_x.add(
+    goto_programt::make_incomplete_goto(true_exprt(), then_end_location));
 
   // do the z label
   goto_programt tmp_z;
-  goto_programt::targett z = tmp_z.add(goto_programt::make_skip());
-  // We deliberately don't set a location for 'z', it's a dummy
-  // target.
+  goto_programt::targett z = tmp_z.add(
+    goto_programt::make_skip(has_else ? else_end_location : then_end_location));
 
   // y: Q;
   goto_programt tmp_y;

Diff for: src/goto-programs/goto_convert_class.h

@@ -578,7 +578,9 @@ class goto_convertt:public messaget
   // if(cond) { true_case } else { false_case }
   void generate_ifthenelse(
     const exprt &cond,
+    const source_locationt &,
     goto_programt &true_case,
+    const source_locationt &,
     goto_programt &false_case,
     const source_locationt &,
     goto_programt &dest,