Skip to content

Commit c830360

Browse files
committed
introduce instructiont::decl_symbol()
This addresses the issue of the ambiguous dual-use of code_declt in both the C front-end and the goto-program API by replacing the use of code_declt by directly returning the symbol_exprt. The client code is simplified.
1 parent a4c81ef commit c830360

21 files changed

+57
-63
lines changed

jbmc/src/java_bytecode/remove_exceptions.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -512,8 +512,7 @@ void remove_exceptionst::instrument_exceptions(
512512
{
513513
if(instr_it->is_decl())
514514
{
515-
code_declt decl = instr_it->get_decl();
516-
locals.push_back(decl.symbol());
515+
locals.push_back(instr_it->decl_symbol());
517516
}
518517
// Is it a handler push/pop or catch landing-pad?
519518
else if(instr_it->type==CATCH)

src/analyses/constant_propagator.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -158,8 +158,7 @@ void constant_propagator_domaint::transform(
158158

159159
if(from->is_decl())
160160
{
161-
const auto &code_decl = from->get_decl();
162-
const symbol_exprt &symbol = code_decl.symbol();
161+
const symbol_exprt &symbol = from->decl_symbol();
163162
values.set_to_top(symbol);
164163
}
165164
else if(from->is_assign())

src/analyses/custom_bitvector_analysis.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -294,12 +294,12 @@ void custom_bitvector_domaint::transform(
294294

295295
case DECL:
296296
{
297-
const code_declt &code_decl=to_code_decl(instruction.code);
298-
assign_lhs(code_decl.symbol(), vectorst());
297+
const auto &decl_symbol = instruction.decl_symbol();
298+
assign_lhs(decl_symbol, vectorst());
299299

300300
// is it a pointer?
301-
if(code_decl.symbol().type().id()==ID_pointer)
302-
assign_lhs(dereference_exprt(code_decl.symbol()), vectorst());
301+
if(decl_symbol.type().id() == ID_pointer)
302+
assign_lhs(dereference_exprt(decl_symbol), vectorst());
303303
}
304304
break;
305305

src/analyses/escape_analysis.cpp

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -202,11 +202,8 @@ void escape_domaint::transform(
202202
break;
203203

204204
case DECL:
205-
{
206-
const code_declt &code_decl=to_code_decl(instruction.code);
207-
aliases.isolate(code_decl.get_identifier());
208-
assign_lhs_cleanup(code_decl.symbol(), std::set<irep_idt>());
209-
}
205+
aliases.isolate(instruction.decl_symbol().get_identifier());
206+
assign_lhs_cleanup(instruction.decl_symbol(), std::set<irep_idt>());
210207
break;
211208

212209
case DEAD:

src/analyses/global_may_alias.cpp

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -120,11 +120,8 @@ void global_may_alias_domaint::transform(
120120
}
121121

122122
case DECL:
123-
{
124-
const code_declt &code_decl = to_code_decl(instruction.code);
125-
aliases.isolate(code_decl.get_identifier());
123+
aliases.isolate(instruction.decl_symbol().get_identifier());
126124
break;
127-
}
128125

129126
case DEAD:
130127
{

src/analyses/goto_rw.cpp

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -822,13 +822,9 @@ void goto_rw(
822822
break;
823823

824824
case DECL:
825+
rw_set.get_objects_rec(function, target, target->decl_symbol().type());
825826
rw_set.get_objects_rec(
826-
function, target, to_code_decl(target->code).symbol().type());
827-
rw_set.get_objects_rec(
828-
function,
829-
target,
830-
rw_range_sett::get_modet::LHS_W,
831-
to_code_decl(target->code).symbol());
827+
function, target, rw_range_sett::get_modet::LHS_W, target->decl_symbol());
832828
break;
833829

834830
case FUNCTION_CALL:

src/analyses/interval_domain.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ void interval_domaint::transform(
7171
switch(instruction.type)
7272
{
7373
case DECL:
74-
havoc_rec(to_code_decl(instruction.code).symbol());
74+
havoc_rec(instruction.decl_symbol());
7575
break;
7676

7777
case DEAD:

src/analyses/local_bitvector_analysis.cpp

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -282,15 +282,12 @@ void local_bitvector_analysist::build()
282282
}
283283

284284
case DECL:
285-
{
286-
const code_declt &code_decl = to_code_decl(instruction.code);
287285
assign_lhs(
288-
code_decl.symbol(),
286+
instruction.decl_symbol(),
289287
exprt(ID_uninitialized),
290288
loc_info_src,
291289
loc_info_dest);
292290
break;
293-
}
294291

295292
case DEAD:
296293
{

src/analyses/local_may_alias.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -383,11 +383,9 @@ void local_may_aliast::build(const goto_functiont &goto_function)
383383
}
384384

385385
case DECL:
386-
{
387-
const code_declt &code_decl = to_code_decl(instruction.code);
388-
assign_lhs(code_decl.symbol(), nil_exprt(), loc_info_src, loc_info_dest);
386+
assign_lhs(
387+
instruction.decl_symbol(), nil_exprt(), loc_info_src, loc_info_dest);
389388
break;
390-
}
391389

392390
case DEAD:
393391
{

src/analyses/locals.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ void localst::build(const goto_functiont &goto_function)
2020
for(const auto &instruction : goto_function.body.instructions)
2121
{
2222
if(instruction.is_decl())
23-
locals.insert(instruction.get_decl().get_identifier());
23+
locals.insert(instruction.decl_symbol().get_identifier());
2424
}
2525

2626
locals.insert(

0 commit comments

Comments
 (0)