Skip to content

Commit 05ed8d9

Browse files
committed
Add user declaration iterators in scope stack
Jumping into scope will may cause these declarations to be executed. Therefore we need to know what the declarations are for each scope in order acheive this.
1 parent c96b3b2 commit 05ed8d9

File tree

1 file changed

+14
-9
lines changed

1 file changed

+14
-9
lines changed

src/goto-programs/goto_convert.cpp

+14-9
Original file line numberDiff line numberDiff line change
@@ -616,22 +616,24 @@ void goto_convertt::convert_frontend_decl(
616616
symbol.type.id()==ID_code)
617617
return; // this is a SKIP!
618618

619-
if(code.operands().size()==1)
620-
{
621-
copy(code, DECL, dest);
622-
}
623-
else
624-
{
619+
const goto_programt::targett declaration_iterator = [&]() {
620+
if(code.operands().size() == 1)
621+
{
622+
copy(code, DECL, dest);
623+
return std::prev(dest.instructions.end());
624+
}
625+
625626
exprt initializer = code.op1();
626627

627-
codet tmp=code;
628+
codet tmp = code;
628629
tmp.operands().resize(1);
629630
// hide this declaration-without-initializer step in the goto trace
630631
tmp.add_source_location().set_hide();
631632

632633
// Break up into decl and assignment.
633634
// Decl must be visible before initializer.
634635
copy(tmp, DECL, dest);
636+
const auto declaration_iterator = std::prev(dest.instructions.end());
635637

636638
auto initializer_location = initializer.find_source_location();
637639
clean_expr(initializer, dest, mode);
@@ -643,7 +645,9 @@ void goto_convertt::convert_frontend_decl(
643645

644646
convert_assign(assign, dest, mode);
645647
}
646-
}
648+
649+
return declaration_iterator;
650+
}();
647651

648652
// now create a 'dead' instruction -- will be added after the
649653
// destructor created below as unwind_destructor_stack pops off the
@@ -652,7 +656,8 @@ void goto_convertt::convert_frontend_decl(
652656

653657
{
654658
code_deadt code_dead(symbol_expr);
655-
targets.scope_stack.add(code_dead, {});
659+
660+
targets.scope_stack.add(code_dead, {declaration_iterator});
656661
}
657662

658663
// do destructor

0 commit comments

Comments
 (0)