Skip to content

Commit f7e5ba6

Browse files
committed
introduce instructiont::dead_symbol()
This mirrors the change in #5861 by replacing the use of code_deadt by directly returning the symbol_exprt. The client code is simplified.
1 parent a4c81ef commit f7e5ba6

File tree

5 files changed

+24
-15
lines changed

5 files changed

+24
-15
lines changed

src/analyses/constant_propagator.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -191,8 +191,7 @@ void constant_propagator_domaint::transform(
191191
}
192192
else if(from->is_dead())
193193
{
194-
const auto &code_dead = from->get_dead();
195-
values.set_to_top(code_dead.symbol());
194+
values.set_to_top(from->dead_symbol());
196195
}
197196
else if(from->is_function_call())
198197
{

src/goto-instrument/goto_program2code.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -94,7 +94,7 @@ void goto_program2codet::build_dead_map()
9494
{
9595
if(instruction.is_dead())
9696
{
97-
dead_map[instruction.get_dead().get_identifier()] =
97+
dead_map[instruction.dead_symbol().get_identifier()] =
9898
instruction.location_number;
9999
}
100100
}

src/goto-programs/goto_program.cpp

Lines changed: 5 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -884,9 +884,9 @@ void goto_programt::instructiont::validate(
884884
source_location);
885885
DATA_CHECK_WITH_DIAGNOSTICS(
886886
vm,
887-
!ns.lookup(get_dead().get_identifier(), table_symbol),
887+
!ns.lookup(dead_symbol().get_identifier(), table_symbol),
888888
"removed symbols should be known",
889-
id2string(get_dead().get_identifier()),
889+
id2string(dead_symbol().get_identifier()),
890890
source_location);
891891
break;
892892
case FUNCTION_CALL:
@@ -966,13 +966,9 @@ void goto_programt::instructiont::transform(
966966

967967
case DEAD:
968968
{
969-
auto new_symbol = f(get_dead().symbol());
969+
auto new_symbol = f(dead_symbol());
970970
if(new_symbol.has_value())
971-
{
972-
auto new_dead = get_dead();
973-
new_dead.symbol() = to_symbol_expr(*new_symbol);
974-
set_dead(new_dead);
975-
}
971+
dead_symbol() = to_symbol_expr(*new_symbol);
976972
}
977973
break;
978974

@@ -1050,7 +1046,7 @@ void goto_programt::instructiont::apply(
10501046
break;
10511047

10521048
case DEAD:
1053-
f(get_dead().symbol());
1049+
f(dead_symbol());
10541050
break;
10551051

10561052
case FUNCTION_CALL:

src/goto-programs/goto_program.h

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -218,13 +218,29 @@ class goto_programt
218218
}
219219

220220
/// Get the dead statement for DEAD
221+
DEPRECATED(SINCE(2021, 2, 24, "Use dead_symbol instead"))
221222
const code_deadt &get_dead() const
222223
{
223224
PRECONDITION(is_dead());
224225
return to_code_dead(code);
225226
}
226227

228+
/// Get the symbol for DEAD
229+
const symbol_exprt &dead_symbol() const
230+
{
231+
PRECONDITION(is_dead());
232+
return to_code_dead(code).symbol();
233+
}
234+
235+
/// Get the symbol for DEAD
236+
symbol_exprt &dead_symbol()
237+
{
238+
PRECONDITION(is_dead());
239+
return to_code_dead(code).symbol();
240+
}
241+
227242
/// Set the dead statement for DEAD
243+
DEPRECATED(SINCE(2021, 2, 24, "Use dead_symbol instead"))
228244
void set_dead(code_deadt c)
229245
{
230246
PRECONDITION(is_dead());

src/goto-symex/symex_dead.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,7 @@ Author: Daniel Kroening, [email protected]
1919
void goto_symext::symex_dead(statet &state)
2020
{
2121
const goto_programt::instructiont &instruction=*state.source.pc;
22-
23-
const code_deadt &code = instruction.get_dead();
24-
symex_dead(state, code.symbol());
22+
symex_dead(state, instruction.dead_symbol());
2523
}
2624

2725
void goto_symext::symex_dead(statet &state, const symbol_exprt &symbol_expr)

0 commit comments

Comments
 (0)