Fix failed coverage in if then else with return statements

regression/cbmc-cover/block-coverage-report1/test.desc

@@ -3,9 +3,8 @@ main.c
 --cover location
 block 1 \(lines main.c:main:3,5\): SATISFIED
 block 2 \(lines main.c:main:6\): SATISFIED
-block 3 \(lines main.c:main:6,9\): FAILED
-block 4 \(lines main.c:main:8\): SATISFIED
-block 5 \(lines main.c:main:9\): SATISFIED
+block 3 \(lines main.c:main:8\): SATISFIED
+block 4 \(lines main.c:main:9\): SATISFIED
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc-cover/built-ins1/test.desc

@@ -3,7 +3,7 @@ main.c
 --cover location --unwind 1
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* 5 of 8 covered
+^\*\* 5 of 7 covered
 --
 ^warning: ignoring
 ^\[.*<builtin-library-

regression/cbmc/destructors/compound_literal.desc

@@ -2,7 +2,7 @@ CORE new-smt-backend
 main.c
 --unwind 10 --show-goto-functions
 activate-multi-line-match
-(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*DEAD .*newAlloc0[\s]*(?P>comment_block)[\s]*DEAD .*pc[\s]*(?P>comment_block)[\s]*DEAD .*literal[\s]*(?P>comment_block)[\s]*9: END_FUNCTION
+(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*DEAD .*newAlloc0[\s]*(?P>comment_block)[\s]*DEAD .*pc[\s]*(?P>comment_block)[\s]*DEAD .*literal[\s]*(?P>comment_block)[\s]*8: END_FUNCTION
 ^EXIT=0$
 ^SIGNAL=0$
 --
@@ -16,7 +16,7 @@ Checks for:
        // 51 file main.c line 44 function main
        DEAD main::$tmp::literal
        // 52 file main.c line 45 function main
-    9: END_FUNCTION
+    8: END_FUNCTION
 
 This asserts that when you've created a compound literal that both temp and real
 variable gets killed.

regression/cbmc/destructors/enter_lexical_block.desc

@@ -2,15 +2,15 @@ CORE new-smt-backend
 main.c
 --unwind 10 --show-goto-functions
 activate-multi-line-match
-(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*6: .*newAlloc4 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc4 := \{ 4 \}[\s]*(?P>comment_block)[\s]*.*newAlloc6 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc6 := \{ 6 \}[\s]*(?P>comment_block)[\s]*.*newAlloc7 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc7 := \{ 7 \}[\s]*(?P>comment_block)[\s]*GOTO 3
+(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*5: .*newAlloc4 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc4 := \{ 4 \}[\s]*(?P>comment_block)[\s]*.*newAlloc6 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc6 := \{ 6 \}[\s]*(?P>comment_block)[\s]*.*newAlloc7 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc7 := \{ 7 \}[\s]*(?P>comment_block)[\s]*GOTO 3
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
 Checks for:
 
        // 37 file main.c line 36 function main
-    6: DECL main::1::2::2::newAlloc4 : struct tag-test
+    5: DECL main::1::2::2::newAlloc4 : struct tag-test
        // 38 file main.c line 36 function main
        ASSIGN main::1::2::2::newAlloc4 := { 4 }
        // 39 file main.c line 37 function main

regression/cprover/loops/while-break1.desc

@@ -3,15 +3,15 @@ while-break1.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S12in\(ς\)$
+^\(\d+\) ∀ ς : state \. S15T\(ς\) ⇒ S12in\(ς\)$
 ^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12in\(ς\)$
 ^\(\d+\) ∀ ς : state \. \(S12in\(ς\) ∧ ¬\(1 ≠ 0\)\) ⇒ S12T\(ς\)$
 ^\(\d+\) ∀ ς : state \. \(S12in\(ς\) ∧ 1 ≠ 0\) ⇒ S12\(ς\)$
-^\(\d+\) ∀ ς : state \. \(S12\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) = 0\)\) ⇒ S13T\(ς\)$
-^\(\d+\) ∀ ς : state \. \(S12\(ς\) ∧ ς\(❝main::1::x❞\) = 0\) ⇒ S13\(ς\)$
-^\(\d+\) ∀ ς : state \. S12T\(ς\) ⇒ S19in\(ς\)$
-^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ S19in\(ς\)$
-^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S19in\(ς\)$
+^\(\d+\) ∀ ς : state \. \(S12\(ς\) ∧ ς\(❝main::1::x❞\) = 0\) ⇒ S13T\(ς\)$
+^\(\d+\) ∀ ς : state \. \(S12\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) = 0\)\) ⇒ S13\(ς\)$
+^\(\d+\) ∀ ς : state \. S12T\(ς\) ⇒ S17in\(ς\)$
+^\(\d+\) ∀ ς : state \. S13T\(ς\) ⇒ S17in\(ς\)$
+^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17in\(ς\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
 --

src/goto-programs/goto_convert.cpp

@@ -1639,13 +1639,28 @@ void goto_convertt::generate_ifthenelse(
   dest.destructive_append(tmp_v);
   dest.destructive_append(tmp_w);
 
+  // When the `then` branch of a balanced `if` condition ends with a `return` or
+  // a `goto` statement, it is not necessary to add the `goto z` and `z:` goto
+  // elements as they are never used.
+  // This helps for example when using `--cover location` as such command are
+  // marked unreachable, but are not part of the user-provided code to analyze.
+  bool then_branch_returns = dest.instructions.rbegin()->is_goto();
+
   if(has_else)
   {
-    dest.destructive_append(tmp_x);
+    // Don't add the `goto` at the end of the `then` branch if not needed
+    if(!then_branch_returns)
+    {
+      dest.destructive_append(tmp_x);
+    }
     dest.destructive_append(tmp_y);
   }
 
-  dest.destructive_append(tmp_z);
+  // Don't add the `z` label at the end of the `if` when not needed.
+  if(!has_else || !then_branch_returns)
+  {
+    dest.destructive_append(tmp_z);
+  }
 }
 
 /// if(guard) goto target;