Skip to content

Commit fe0b892

Browse files
committed
code_deadt operand is now typed
the operand of code_deadt is now enforced to be symbol_exprt; this saves conversions when used.
1 parent 3028bf8 commit fe0b892

File tree

7 files changed

+22
-25
lines changed

7 files changed

+22
-25
lines changed

src/analyses/constant_propagator.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,7 @@ void constant_propagator_domaint::transform(
132132
else if(from->is_dead())
133133
{
134134
const code_deadt &code_dead=to_code_dead(from->code);
135-
values.set_to_top(to_symbol_expr(code_dead.symbol()));
135+
values.set_to_top(code_dead.symbol());
136136
}
137137
else if(from->is_function_call())
138138
{

src/analyses/reaching_definitions.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -128,8 +128,7 @@ void rd_range_domaint::transform_dead(
128128
const namespacet &,
129129
locationt from)
130130
{
131-
const irep_idt &identifier=
132-
to_symbol_expr(to_code_dead(from->code).symbol()).get_identifier();
131+
const irep_idt &identifier = to_code_dead(from->code).get_identifier();
133132

134133
valuest::iterator entry=values.find(identifier);
135134

src/goto-diff/change_impact.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -85,8 +85,8 @@ void full_slicert::operator()(
8585
}
8686
else if(e_it->first->is_dead())
8787
{
88-
const exprt &s=to_code_dead(e_it->first->code).symbol();
89-
decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);
88+
const auto &s=to_code_dead(e_it->first->code).symbol();
89+
decl_dead[s.get_identifier()].push(e_it->second);
9090
}
9191
}
9292

src/goto-instrument/full_slicer.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -315,8 +315,8 @@ void full_slicert::operator()(
315315
}
316316
else if(e_it->first->is_dead())
317317
{
318-
const exprt &s=to_code_dead(e_it->first->code).symbol();
319-
decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);
318+
const auto &s = to_code_dead(e_it->first->code).symbol();
319+
decl_dead[s.get_identifier()].push(e_it->second);
320320
}
321321
}
322322

src/goto-symex/symex_dead.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ void goto_symext::symex_dead(statet &state)
2626
// We increase the L2 renaming to make these non-deterministic.
2727
// We also prevent propagation of old values.
2828

29-
ssa_exprt ssa(to_symbol_expr(code.symbol()));
29+
ssa_exprt ssa(code.symbol());
3030
state.rename(ssa, ns, goto_symex_statet::L1);
3131

3232
// in case of pointers, put something into the value set

src/util/std_code.cpp

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -18,11 +18,6 @@ const irep_idt &code_declt::get_identifier() const
1818
return to_symbol_expr(symbol()).get_identifier();
1919
}
2020

21-
const irep_idt &code_deadt::get_identifier() const
22-
{
23-
return to_symbol_expr(symbol()).get_identifier();
24-
}
25-
2621
/// If this `codet` is a \ref code_blockt (i.e.\ it represents a block of
2722
/// statements), return the unmodified input. Otherwise (i.e.\ the `codet`
2823
/// represents a single statement), convert it to a \ref code_blockt with the

src/util/std_code.h

Lines changed: 15 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,9 @@ Author: Daniel Kroening, [email protected]
1212

1313
#include <list>
1414

15-
#include "expr.h"
1615
#include "expr_cast.h"
1716
#include "invariant.h"
17+
#include "std_expr.h"
1818

1919
/// Data structure for representing an arbitrary statement in a program. Every
2020
/// specific type of statement (e.g. block of statements, assignment,
@@ -338,28 +338,25 @@ inline code_declt &to_code_decl(codet &code)
338338
class code_deadt:public codet
339339
{
340340
public:
341-
DEPRECATED("use code_deadt(symbol) instead")
342-
code_deadt():codet(ID_dead)
341+
explicit code_deadt(const symbol_exprt &symbol) : codet(ID_dead)
343342
{
344-
operands().resize(1);
343+
add_to_operands(symbol);
345344
}
346345

347-
explicit code_deadt(const exprt &symbol):codet(ID_dead)
346+
symbol_exprt &symbol()
348347
{
349-
copy_to_operands(symbol);
348+
return static_cast<symbol_exprt &>(op0());
350349
}
351350

352-
exprt &symbol()
351+
const symbol_exprt &symbol() const
353352
{
354-
return op0();
353+
return static_cast<const symbol_exprt &>(op0());
355354
}
356355

357-
const exprt &symbol() const
356+
const irep_idt &get_identifier() const
358357
{
359-
return op0();
358+
return symbol().get_identifier();
360359
}
361-
362-
const irep_idt &get_identifier() const;
363360
};
364361

365362
template<> inline bool can_cast_expr<code_deadt>(const exprt &base)
@@ -377,6 +374,9 @@ inline const code_deadt &to_code_dead(const codet &code)
377374
PRECONDITION(code.get_statement() == ID_dead);
378375
DATA_INVARIANT(
379376
code.operands().size() == 1, "dead statement must have one operand");
377+
DATA_INVARIANT(
378+
to_unary_expr(code).op().id() == ID_symbol,
379+
"dead statement must take symbol operand");
380380
return static_cast<const code_deadt &>(code);
381381
}
382382

@@ -385,6 +385,9 @@ inline code_deadt &to_code_dead(codet &code)
385385
PRECONDITION(code.get_statement() == ID_dead);
386386
DATA_INVARIANT(
387387
code.operands().size() == 1, "dead statement must have one operand");
388+
DATA_INVARIANT(
389+
to_unary_expr(code).op().id() == ID_symbol,
390+
"dead statement must take symbol operand");
388391
return static_cast<code_deadt &>(code);
389392
}
390393

0 commit comments

Comments
 (0)