diff --git a/regression/cbmc/destructors/enter_lexical_block.desc b/regression/cbmc/destructors/enter_lexical_block.desc index 296188dd84f..dd4f1e34852 100644 --- a/regression/cbmc/destructors/enter_lexical_block.desc +++ b/regression/cbmc/destructors/enter_lexical_block.desc @@ -2,7 +2,7 @@ CORE main.c --unwind 10 --show-goto-functions activate-multi-line-match -(?P\/\/ [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\/\/ [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. diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 172f1b3f0dc..f1cdce715ed 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/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