Skip to content

Commit 25c097e

Browse files
author
Daniel Kroening
committed
use get_identifier() instead of get(ID_identifier) on symbols
1 parent 70f13f3 commit 25c097e

30 files changed

+161
-99
lines changed

‎src/analyses/ai.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -462,7 +462,7 @@ bool ai_baset::do_function_call_rec(
462462

463463
if(function.id()==ID_symbol)
464464
{
465-
const irep_idt &identifier=function.get(ID_identifier);
465+
const irep_idt &identifier = to_symbol_expr(function).get_identifier();
466466

467467
goto_functionst::function_mapt::const_iterator it=
468468
goto_functions.function_map.find(identifier);

‎src/analyses/flow_insensitive_analysis.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -293,7 +293,7 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
293293

294294
if(function.id()==ID_symbol)
295295
{
296-
const irep_idt &identifier=function.get(ID_identifier);
296+
const irep_idt &identifier = to_symbol_expr(function).get_identifier();
297297

298298
if(recursion_set.find(identifier)!=recursion_set.end())
299299
{

‎src/analyses/invariant_set.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -143,7 +143,7 @@ std::string inv_object_storet::build_string(const exprt &expr) const
143143
}
144144

145145
if(expr.id()==ID_symbol)
146-
return expr.get_string(ID_identifier);
146+
return id2string(to_symbol_expr(expr).get_identifier());
147147

148148
return "";
149149
}

‎src/analyses/static_analysis.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -328,7 +328,7 @@ void static_analysis_baset::do_function_call_rec(
328328

329329
if(function.id()==ID_symbol)
330330
{
331-
const irep_idt &identifier=function.get(ID_identifier);
331+
const irep_idt &identifier = to_symbol_expr(function).get_identifier();
332332

333333
if(recursion_set.find(identifier)!=recursion_set.end())
334334
{

‎src/ansi-c/c_typecast.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -262,8 +262,8 @@ typet c_typecastt::follow_with_qualifiers(const typet &src_type)
262262

263263
while(result_type.id()==ID_symbol)
264264
{
265-
const symbolt &followed_type_symbol=
266-
ns.lookup(result_type.get(ID_identifier));
265+
const symbolt &followed_type_symbol =
266+
ns.lookup(to_symbol_type(result_type));
267267

268268
result_type=followed_type_symbol.type;
269269
qualifiers+=c_qualifierst(followed_type_symbol.type);

‎src/ansi-c/type2name.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
1515
#include <util/invariant.h>
1616
#include <util/namespace.h>
1717
#include <util/pointer_offset_size.h>
18+
#include <util/std_expr.h>
1819
#include <util/std_types.h>
1920
#include <util/symbol_table.h>
2021

@@ -180,7 +181,7 @@ static std::string type2name(
180181
const array_typet &t=to_array_type(type);
181182
mp_integer size;
182183
if(t.size().id()==ID_symbol)
183-
result+="ARR"+id2string(t.size().get(ID_identifier));
184+
result += "ARR" + id2string(to_symbol_expr(t.size()).get_identifier());
184185
else if(to_integer(t.size(), size))
185186
result+="ARR?";
186187
else

‎src/cpp/cpp_is_pod.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -82,8 +82,8 @@ bool cpp_typecheckt::cpp_is_pod(const typet &type) const
8282
}
8383
else if(type.id()==ID_symbol)
8484
{
85-
const symbolt &symb=lookup(type.get(ID_identifier));
86-
assert(symb.is_type);
85+
const symbolt &symb = lookup(to_symbol_type(type));
86+
DATA_INVARIANT(symb.is_type, "type symbol is a type");
8787
return cpp_is_pod(symb.type);
8888
}
8989

‎src/cpp/cpp_typecheck_resolve.cpp

+6-6
Original file line numberDiff line numberDiff line change
@@ -170,9 +170,9 @@ void cpp_typecheck_resolvet::remove_duplicates(
170170
irep_idt id;
171171

172172
if(it->id()==ID_symbol)
173-
id=it->get(ID_identifier);
173+
id = to_symbol_expr(*it).get_identifier();
174174
else if(it->id()==ID_type && it->type().id()==ID_symbol)
175-
id=it->type().get(ID_identifier);
175+
id = to_symbol_type(it->type()).get_identifier();
176176

177177
if(id=="")
178178
{
@@ -2041,8 +2041,8 @@ void cpp_typecheck_resolvet::apply_template_args(
20412041
if(expr.id()!=ID_symbol)
20422042
return; // templates are always symbols
20432043

2044-
const symbolt &template_symbol=
2045-
cpp_typecheck.lookup(expr.get(ID_identifier));
2044+
const symbolt &template_symbol =
2045+
cpp_typecheck.lookup(to_symbol_expr(expr).get_identifier());
20462046

20472047
if(!template_symbol.type.get_bool(ID_is_template))
20482048
return;
@@ -2239,7 +2239,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
22392239
const typet &type=pcomp.type();
22402240
assert(type.id()!=ID_struct);
22412241
if(type.id()==ID_symbol)
2242-
identifier=type.get(ID_identifier);
2242+
identifier = to_symbol_type(type).get_identifier();
22432243
else
22442244
continue;
22452245
}
@@ -2261,7 +2261,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
22612261
break;
22622262
}
22632263
else if(symbol.type.id()==ID_symbol)
2264-
identifier=symbol.type.get(ID_identifier);
2264+
identifier = to_symbol_type(symbol.type).get_identifier();
22652265
else
22662266
break;
22672267
}

‎src/cpp/template_map.cpp

+6-4
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
1414
#include <ostream>
1515

1616
#include <util/invariant.h>
17+
#include <util/std_expr.h>
18+
#include <util/std_types.h>
1719

1820
void template_mapt::apply(typet &type) const
1921
{
@@ -39,8 +41,8 @@ void template_mapt::apply(typet &type) const
3941
}
4042
else if(type.id()==ID_symbol)
4143
{
42-
type_mapt::const_iterator m_it=
43-
type_map.find(type.get(ID_identifier));
44+
type_mapt::const_iterator m_it =
45+
type_map.find(to_symbol_type(type).get_identifier());
4446

4547
if(m_it!=type_map.end())
4648
{
@@ -73,8 +75,8 @@ void template_mapt::apply(exprt &expr) const
7375

7476
if(expr.id()==ID_symbol)
7577
{
76-
expr_mapt::const_iterator m_it=
77-
expr_map.find(expr.get(ID_identifier));
78+
expr_mapt::const_iterator m_it =
79+
expr_map.find(to_symbol_expr(expr).get_identifier());
7880

7981
if(m_it!=expr_map.end())
8082
{

‎src/goto-programs/builtin_functions.cpp

+11-11
Original file line numberDiff line numberDiff line change
@@ -29,11 +29,11 @@ Author: Daniel Kroening, [email protected]
2929

3030
void goto_convertt::do_prob_uniform(
3131
const exprt &lhs,
32-
const exprt &function,
32+
const symbol_exprt &function,
3333
const exprt::operandst &arguments,
3434
goto_programt &dest)
3535
{
36-
const irep_idt &identifier=function.get(ID_identifier);
36+
const irep_idt &identifier = function.get_identifier();
3737

3838
// make it a side effect if there is an LHS
3939
if(arguments.size()!=2)
@@ -107,11 +107,11 @@ void goto_convertt::do_prob_uniform(
107107

108108
void goto_convertt::do_prob_coin(
109109
const exprt &lhs,
110-
const exprt &function,
110+
const symbol_exprt &function,
111111
const exprt::operandst &arguments,
112112
goto_programt &dest)
113113
{
114-
const irep_idt &identifier=function.get(ID_identifier);
114+
const irep_idt &identifier = function.get_identifier();
115115

116116
// make it a side effect if there is an LHS
117117
if(arguments.size()!=2)
@@ -184,11 +184,11 @@ void goto_convertt::do_prob_coin(
184184

185185
void goto_convertt::do_printf(
186186
const exprt &lhs,
187-
const exprt &function,
187+
const symbol_exprt &function,
188188
const exprt::operandst &arguments,
189189
goto_programt &dest)
190190
{
191-
const irep_idt &f_id=function.get(ID_identifier);
191+
const irep_idt &f_id = function.get_identifier();
192192

193193
if(f_id==CPROVER_PREFIX "printf" ||
194194
f_id=="printf")
@@ -219,11 +219,11 @@ void goto_convertt::do_printf(
219219

220220
void goto_convertt::do_scanf(
221221
const exprt &lhs,
222-
const exprt &function,
222+
const symbol_exprt &function,
223223
const exprt::operandst &arguments,
224224
goto_programt &dest)
225225
{
226-
const irep_idt &f_id=function.get(ID_identifier);
226+
const irep_idt &f_id = function.get_identifier();
227227

228228
if(f_id==CPROVER_PREFIX "scanf")
229229
{
@@ -364,7 +364,7 @@ void goto_convertt::do_output(
364364

365365
void goto_convertt::do_atomic_begin(
366366
const exprt &lhs,
367-
const exprt &function,
367+
const symbol_exprt &function,
368368
const exprt::operandst &arguments,
369369
goto_programt &dest)
370370
{
@@ -388,7 +388,7 @@ void goto_convertt::do_atomic_begin(
388388

389389
void goto_convertt::do_atomic_end(
390390
const exprt &lhs,
391-
const exprt &function,
391+
const symbol_exprt &function,
392392
const exprt::operandst &arguments,
393393
goto_programt &dest)
394394
{
@@ -597,7 +597,7 @@ exprt goto_convertt::get_array_argument(const exprt &src)
597597
void goto_convertt::do_array_op(
598598
const irep_idt &id,
599599
const exprt &lhs,
600-
const exprt &function,
600+
const symbol_exprt &function,
601601
const exprt::operandst &arguments,
602602
goto_programt &dest)
603603
{

‎src/goto-programs/goto_convert.cpp

+5-5
Original file line numberDiff line numberDiff line change
@@ -657,16 +657,16 @@ void goto_convertt::convert_decl(
657657
goto_programt &dest,
658658
const irep_idt &mode)
659659
{
660-
const exprt &op0=code.op0();
660+
const exprt &op = code.symbol();
661661

662-
if(op0.id()!=ID_symbol)
662+
if(op.id() != ID_symbol)
663663
{
664-
error().source_location=op0.find_source_location();
665-
error() << "decl statement expects symbol as first operand" << eom;
664+
error().source_location = op.find_source_location();
665+
error() << "decl statement expects symbol as operand" << eom;
666666
throw 0;
667667
}
668668

669-
const irep_idt &identifier=op0.get(ID_identifier);
669+
const irep_idt &identifier = to_symbol_expr(op).get_identifier();
670670

671671
const symbolt &symbol = ns.lookup(identifier);
672672

‎src/goto-programs/goto_convert_class.h

+9-9
Original file line numberDiff line numberDiff line change
@@ -606,38 +606,38 @@ class goto_convertt:public messaget
606606
// some built-in functions
607607
void do_atomic_begin(
608608
const exprt &lhs,
609-
const exprt &rhs,
609+
const symbol_exprt &function,
610610
const exprt::operandst &arguments,
611611
goto_programt &dest);
612612
void do_atomic_end(
613613
const exprt &lhs,
614-
const exprt &rhs,
614+
const symbol_exprt &function,
615615
const exprt::operandst &arguments,
616616
goto_programt &dest);
617617
void do_create_thread(
618618
const exprt &lhs,
619-
const exprt &rhs,
619+
const symbol_exprt &function,
620620
const exprt::operandst &arguments,
621621
goto_programt &dest);
622622
void do_array_equal(
623623
const exprt &lhs,
624-
const exprt &rhs,
624+
const symbol_exprt &rhs,
625625
const exprt::operandst &arguments,
626626
goto_programt &dest);
627627
void do_array_op(
628628
const irep_idt &id,
629629
const exprt &lhs,
630-
const exprt &function,
630+
const symbol_exprt &function,
631631
const exprt::operandst &arguments,
632632
goto_programt &dest);
633633
void do_printf(
634634
const exprt &lhs,
635-
const exprt &rhs,
635+
const symbol_exprt &function,
636636
const exprt::operandst &arguments,
637637
goto_programt &dest);
638638
void do_scanf(
639639
const exprt &lhs,
640-
const exprt &rhs,
640+
const symbol_exprt &function,
641641
const exprt::operandst &arguments,
642642
goto_programt &dest);
643643
void do_input(
@@ -652,12 +652,12 @@ class goto_convertt:public messaget
652652
goto_programt &dest);
653653
void do_prob_coin(
654654
const exprt &lhs,
655-
const exprt &rhs,
655+
const symbol_exprt &function,
656656
const exprt::operandst &arguments,
657657
goto_programt &dest);
658658
void do_prob_uniform(
659659
const exprt &lhs,
660-
const exprt &rhs,
660+
const symbol_exprt &function,
661661
const exprt::operandst &arguments,
662662
goto_programt &dest);
663663

‎src/goto-programs/goto_convert_side_effect.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -373,7 +373,7 @@ void goto_convertt::remove_function_call(
373373

374374
if(expr.op0().id()==ID_symbol)
375375
{
376-
const irep_idt &identifier=expr.op0().get(ID_identifier);
376+
const irep_idt &identifier = to_symbol_expr(expr.op0()).get_identifier();
377377
const symbolt &symbol = ns.lookup(identifier);
378378

379379
new_base_name+='_';

‎src/goto-programs/interpreter.cpp

+4-2
Original file line numberDiff line numberDiff line change
@@ -837,8 +837,9 @@ void interpretert::execute_function_call()
837837
}
838838
else
839839
{
840-
list_input_varst::iterator it=
841-
function_input_vars.find(function_call.function().get(ID_identifier));
840+
list_input_varst::iterator it = function_input_vars.find(
841+
to_symbol_expr(function_call.function()).get_identifier());
842+
842843
if(it!=function_input_vars.end())
843844
{
844845
mp_vectort value;
@@ -852,6 +853,7 @@ void interpretert::execute_function_call()
852853
it->second.pop_front();
853854
return;
854855
}
856+
855857
if(show)
856858
error() << "no body for "+id2string(identifier) << eom;
857859
}

‎src/goto-programs/interpreter_evaluate.cpp

+3-4
Original file line numberDiff line numberDiff line change
@@ -1083,10 +1083,9 @@ mp_integer interpretert::evaluate_address(
10831083
{
10841084
if(expr.id()==ID_symbol)
10851085
{
1086-
const irep_idt &identifier=
1087-
is_ssa_expr(expr) ?
1088-
to_ssa_expr(expr).get_original_name() :
1089-
expr.get(ID_identifier);
1086+
const irep_idt &identifier = is_ssa_expr(expr)
1087+
? to_ssa_expr(expr).get_original_name()
1088+
: to_symbol_expr(expr).get_identifier();
10901089

10911090
interpretert::memory_mapt::const_iterator m_it1=
10921091
memory_map.find(identifier);

‎src/goto-programs/json_goto_trace.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -107,7 +107,8 @@ void convert_decl(
107107
{
108108
if(expr.id() == ID_symbol)
109109
{
110-
const symbolt &symbol = ns.lookup(expr.get(ID_identifier));
110+
const symbolt &symbol = ns.lookup(to_symbol_expr(expr));
111+
111112
if(expr.find(ID_C_base_name).is_not_nil())
112113
INVARIANT(
113114
expr.find(ID_C_base_name).id() == symbol.base_name,

‎src/goto-programs/remove_const_function_pointers.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -72,8 +72,8 @@ exprt remove_const_function_pointerst::replace_const_symbols(
7272
{
7373
if(is_const_expression(expression))
7474
{
75-
const symbolt &symbol=
76-
*symbol_table.lookup(expression.get(ID_identifier));
75+
const symbolt &symbol =
76+
*symbol_table.lookup(to_symbol_expr(expression).get_identifier());
7777
if(symbol.type.id()!=ID_code)
7878
{
7979
const exprt &symbol_value=symbol.value;

‎src/goto-programs/remove_unused_functions.cpp

+4-3
Original file line numberDiff line numberDiff line change
@@ -81,9 +81,10 @@ void find_used_functions(
8181
// check that this is actually a simple call
8282
assert(call.function().id()==ID_symbol);
8383

84-
find_used_functions(call.function().get(ID_identifier),
85-
functions,
86-
seen);
84+
const irep_idt &identifier =
85+
to_symbol_expr(call.function()).get_identifier();
86+
87+
find_used_functions(identifier, functions, seen);
8788
}
8889
}
8990
}

0 commit comments

Comments
 (0)