Variables leaving scope on jumping should always be marked dead

Even if new variables would be introduced to the scope, the existing
variables which go out of scope still need to be marked as dead and/or
have their destructors called.

The placeholder for construction is moved to after the destruction, as
destructions should be done first.

Author: thomasspriggs

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