Variables leaving scope on jumping should always be marked dead

regression/cbmc/destructors/enter_lexical_block.desc

@@ -2,7 +2,7 @@ CORE
 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]*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
+(?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]*.*DEAD main::1::2::2::newAlloc7[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc6[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc4[\s]*(?P>comment_block)[\s]*.*GOTO 3
 ^EXIT=0$
 ^SIGNAL=0$
 --
@@ -22,8 +22,14 @@ Checks for:
        // 42 file main.c line 38 function main
        ASSIGN main::1::2::2::newAlloc7 := { 7 }
        // 43 file main.c line 39 function main
+       DEAD main::1::2::2::newAlloc7
+       // 44 file main.c line 39 function main
+       DEAD main::1::2::2::newAlloc6
+       // 45 file main.c line 39 function main
+       DEAD main::1::2::2::newAlloc4
+       // 46 file main.c line 39 function main
        GOTO 3
 
 This asserts that when the GOTO is going into a lexical block that destructors
-are omitted. This used to be a limitation with the previous implementation and should
-now be fixable, but for consistency it acts in the same way.
+are not omitted. This used to be a limitation with the previous implementation
+and has now been fixed.

src/goto-programs/goto_convert.cpp

@@ -151,42 +151,40 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
         targets.destructor_stack.get_nearest_common_ancestor_info(
           goto_target, label_target);
 
-      bool not_prefix =
-        intersection_result.right_depth_below_common_ancestor != 0;
-
       // If our goto had no variables of note, just skip
       if(goto_target != 0)
       {
         // If the goto recorded a destructor stack, execute as much as is
         // appropriate for however many automatic variables leave scope.
-        // We don't currently handle variables *entering* scope, which
-        // is illegal for C++ non-pod types and impossible in Java in any case.
-        if(not_prefix)
-        {
-          debug().source_location = i.source_location();
-          debug() << "encountered goto '" << goto_label
-                  << "' that enters one or more lexical blocks; "
-                  << "omitting constructors and destructors" << eom;
-        }
-        else
-        {
-          debug().source_location = i.source_location();
-          debug() << "adding goto-destructor code on jump to '" << goto_label
-                  << "'" << eom;
-
-          node_indext end_destruct = intersection_result.common_ancestor;
-          goto_programt destructor_code;
-          unwind_destructor_stack(
-            i.source_location(),
-            destructor_code,
-            mode,
-            end_destruct,
-            goto_target);
-          dest.destructive_insert(g_it.first, destructor_code);
-
-          // This should leave iterators intact, as long as
-          // goto_programt::instructionst is std::list.
-        }
+        debug().source_location = i.source_location();
+        debug() << "adding goto-destructor code on jump to '" << goto_label
+                << "'" << eom;
+
+        node_indext end_destruct = intersection_result.common_ancestor;
+        goto_programt destructor_code;
+        unwind_destructor_stack(
+          i.source_location(),
+          destructor_code,
+          mode,
+          end_destruct,
+          goto_target);
+        dest.destructive_insert(g_it.first, destructor_code);
+
+        // This should leave iterators intact, as long as
+        // goto_programt::instructionst is std::list.
+      }
+
+      // We don't currently handle variables *entering* scope, which
+      // is illegal for C++ non-pod types and impossible in Java in any case.
+      // This is however valid C.
+      const bool variables_added_to_scope =
+        intersection_result.right_depth_below_common_ancestor > 0;
+      if(variables_added_to_scope)
+      {
+        debug().source_location = i.source_location();
+        debug() << "encountered goto '" << goto_label
+                << "' that enters one or more lexical blocks; "
+                << "omitting constructors." << eom;
       }
     }
     else