Skip to content

Commit 811a601

Browse files
authored
Merge pull request #4437 from smowton/smowton/cleanup/symbol-table-ref-methods
Use symbol_tablet::lookup_ref and ::get_writeable_ref
2 parents 08dfd8d + 78c1c31 commit 811a601

25 files changed

+42
-43
lines changed

jbmc/src/java_bytecode/java_bytecode_typecheck.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -52,14 +52,14 @@ void java_bytecode_typecheckt::typecheck(
5252
// recursively doing base classes first.
5353
for(const irep_idt &id : identifiers)
5454
{
55-
symbolt &symbol=*symbol_table.get_writeable(id);
55+
symbolt &symbol = symbol_table.get_writeable_ref(id);
5656
if(symbol.is_type)
5757
typecheck_type_symbol(symbol);
5858
}
5959
// We now check all non-type symbols
6060
for(const irep_idt &id : identifiers)
6161
{
62-
symbolt &symbol=*symbol_table.get_writeable(id);
62+
symbolt &symbol = symbol_table.get_writeable_ref(id);
6363
if(!symbol.is_type)
6464
typecheck_non_type_symbol(symbol);
6565
}

jbmc/src/java_bytecode/java_entry_point.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -125,7 +125,8 @@ static void java_static_lifetime_init(
125125
bool string_refinement_enabled,
126126
message_handlert &message_handler)
127127
{
128-
symbolt &initialize_symbol=*symbol_table.get_writeable(INITIALIZE_FUNCTION);
128+
symbolt &initialize_symbol =
129+
symbol_table.get_writeable_ref(INITIALIZE_FUNCTION);
129130
code_blockt &code_block=to_code_block(to_code(initialize_symbol.value));
130131
object_factory_parameters.function_id = initialize_symbol.name;
131132

@@ -160,7 +161,7 @@ static void java_static_lifetime_init(
160161
++symbol_it)
161162
{
162163
const auto &symname = *symbol_it;
163-
const symbolt &sym=*symbol_table.lookup(symname);
164+
const symbolt &sym = symbol_table.lookup_ref(symname);
164165
if(should_init_symbol(sym))
165166
{
166167
if(const symbolt *class_literal_init_method =
@@ -468,7 +469,7 @@ static optionalt<codet> record_return_value(
468469
return {};
469470

470471
const symbolt &return_symbol =
471-
*symbol_table.lookup(JAVA_ENTRY_POINT_RETURN_SYMBOL);
472+
symbol_table.lookup_ref(JAVA_ENTRY_POINT_RETURN_SYMBOL);
472473

473474
codet output(ID_output);
474475
output.operands().resize(2);
@@ -493,7 +494,7 @@ static code_blockt record_pointer_parameters(
493494
param_number++)
494495
{
495496
const symbolt &p_symbol =
496-
*symbol_table.lookup(parameters[param_number].get_identifier());
497+
symbol_table.lookup_ref(parameters[param_number].get_identifier());
497498

498499
if(!can_cast_type<pointer_typet>(p_symbol.type))
499500
continue;

jbmc/src/java_bytecode/java_utils.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -365,8 +365,8 @@ get_inherited_component(
365365
return *resolved_component;
366366

367367
// No, may be inherited from some parent class; check it is visible:
368-
const symbolt &component_symbol =
369-
*symbol_table.lookup(resolved_component->get_full_component_identifier());
368+
const symbolt &component_symbol = symbol_table.lookup_ref(
369+
resolved_component->get_full_component_identifier());
370370

371371
irep_idt access = component_symbol.type.get(ID_access);
372372
if(access.empty())

jbmc/src/java_bytecode/simple_method_stubbing.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -235,7 +235,7 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
235235
/// \param symname: Symbol name to consider stubbing
236236
void java_simple_method_stubst::check_method_stub(const irep_idt &symname)
237237
{
238-
const symbolt &sym = *symbol_table.lookup(symname);
238+
const symbolt &sym = symbol_table.lookup_ref(symname);
239239
if(!sym.is_type && sym.value.id() == ID_nil &&
240240
sym.type.id() == ID_code &&
241241
// do not stub internal locking calls as 'create_method_stub' does not
@@ -248,7 +248,7 @@ void java_simple_method_stubst::check_method_stub(const irep_idt &symname)
248248
sym.name !=
249249
"java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V")
250250
{
251-
create_method_stub(*symbol_table.get_writeable(symname));
251+
create_method_stub(symbol_table.get_writeable_ref(symname));
252252
}
253253
}
254254

src/ansi-c/ansi_c_entry_point.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ void record_function_outputs(
6363
codet output(ID_output);
6464
output.operands().resize(2);
6565

66-
const symbolt &return_symbol=*symbol_table.lookup("return'");
66+
const symbolt &return_symbol = symbol_table.lookup_ref("return'");
6767

6868
output.op0()=
6969
address_of_exprt(

src/ansi-c/c_typecheck_base.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -125,7 +125,7 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
125125
throw 0;
126126
}
127127

128-
symbolt & existing_symbol=*symbol_table.get_writeable(symbol.name);
128+
symbolt &existing_symbol = symbol_table.get_writeable_ref(symbol.name);
129129
if(symbol.is_type)
130130
typecheck_redefinition_type(existing_symbol, symbol);
131131
else
@@ -735,7 +735,7 @@ void c_typecheck_baset::typecheck_declaration(
735735
// add code contract (if any); we typecheck this after the
736736
// function body done above, so as to have parameter symbols
737737
// available
738-
symbolt &new_symbol=*symbol_table.get_writeable(identifier);
738+
symbolt &new_symbol = symbol_table.get_writeable_ref(identifier);
739739

740740
typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_requires);
741741

src/cpp/cpp_instantiate_template.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -369,7 +369,7 @@ const symbolt &cpp_typecheckt::instantiate_template(
369369
// been instantiated using these arguments
370370
{
371371
// need non-const handle on template symbol
372-
symbolt &s=*symbol_table.get_writeable(template_symbol.name);
372+
symbolt &s = symbol_table.get_writeable_ref(template_symbol.name);
373373
irept &instantiated_with = s.value.add(ID_instantiated_with);
374374
instantiated_with.get_sub().push_back(specialization_template_args);
375375
}
@@ -461,7 +461,7 @@ const symbolt &cpp_typecheckt::instantiate_template(
461461

462462
if(is_template_method)
463463
{
464-
symbolt &symb=*symbol_table.get_writeable(class_name);
464+
symbolt &symb = symbol_table.get_writeable_ref(class_name);
465465

466466
assert(new_decl.declarators().size() == 1);
467467

src/cpp/cpp_typecheck.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -156,7 +156,7 @@ void cpp_typecheckt::static_and_dynamic_initialization()
156156

157157
for(const irep_idt &d_it : dynamic_initializations)
158158
{
159-
const symbolt &symbol=*symbol_table.lookup(d_it);
159+
const symbolt &symbol = symbol_table.lookup_ref(d_it);
160160

161161
if(symbol.is_extern)
162162
continue;
@@ -250,7 +250,7 @@ void cpp_typecheckt::do_not_typechecked()
250250
UNREACHABLE; // Don't know what to do!
251251

252252
symbolt &writable_symbol =
253-
*symbol_table.get_writeable(named_symbol.first);
253+
symbol_table.get_writeable_ref(named_symbol.first);
254254
writable_symbol.value.swap(value);
255255
convert_function(writable_symbol);
256256
}

src/cpp/cpp_typecheck_compound_type.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -194,7 +194,7 @@ void cpp_typecheckt::typecheck_compound_type(
194194
to_struct_union_type(symbol.type).is_incomplete())
195195
{
196196
// a previously incomplete struct/union becomes complete
197-
symbolt &writeable_symbol = *symbol_table.get_writeable(symbol_name);
197+
symbolt &writeable_symbol = symbol_table.get_writeable_ref(symbol_name);
198198
writeable_symbol.type.swap(type);
199199
typecheck_compound_body(writeable_symbol);
200200
}
@@ -1426,8 +1426,8 @@ void cpp_typecheckt::convert_anon_struct_union_member(
14261426
const irep_idt &access,
14271427
struct_typet::componentst &components)
14281428
{
1429-
symbolt &struct_union_symbol=
1430-
*symbol_table.get_writeable(follow(declaration.type()).get(ID_name));
1429+
symbolt &struct_union_symbol =
1430+
symbol_table.get_writeable_ref(follow(declaration.type()).get(ID_name));
14311431

14321432
if(declaration.storage_spec().is_static() ||
14331433
declaration.storage_spec().is_mutable())

src/cpp/cpp_typecheck_declaration.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -58,8 +58,8 @@ codet cpp_typecheckt::convert_anonymous_union(cpp_declarationt &declaration)
5858
new_code.add_to_operands(code_declt(cpp_symbol_expr(symbol)));
5959

6060
// do scoping
61-
symbolt union_symbol=
62-
*symbol_table.get_writeable(follow(symbol.type).get(ID_name));
61+
symbolt union_symbol =
62+
symbol_table.get_writeable_ref(follow(symbol.type).get(ID_name));
6363

6464
for(const auto &c : to_union_type(union_symbol.type).components())
6565
{

src/cpp/cpp_typecheck_template.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -377,8 +377,7 @@ void cpp_typecheckt::typecheck_class_template_member(
377377
}
378378

379379
const cpp_idt &cpp_id=**(id_set.begin());
380-
symbolt &template_symbol=
381-
*symbol_table.get_writeable(cpp_id.identifier);
380+
symbolt &template_symbol = symbol_table.get_writeable_ref(cpp_id.identifier);
382381

383382
exprt &template_methods =
384383
static_cast<exprt &>(template_symbol.value.add(ID_template_methods));

src/goto-instrument/accelerate/accelerate.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -427,7 +427,7 @@ bool acceleratet::is_underapproximate(path_acceleratort &accelerator)
427427
if(it->id()==ID_symbol && it->type() == bool_typet())
428428
{
429429
const irep_idt &id=to_symbol_expr(*it).get_identifier();
430-
const symbolt &sym=*symbol_table.lookup(id);
430+
const symbolt &sym = symbol_table.lookup_ref(id);
431431

432432
if(sym.module=="scratch")
433433
{

src/goto-instrument/accelerate/acceleration_utils.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -227,7 +227,7 @@ void acceleration_utilst::stash_variables(
227227
it!=vars.end();
228228
++it)
229229
{
230-
symbolt orig=*symbol_table.lookup(*it);
230+
const symbolt &orig = symbol_table.lookup_ref(*it);
231231
symbolt stashed_sym=fresh_symbol("polynomial::stash", orig.type);
232232
substitution[orig.symbol_expr()]=stashed_sym.symbol_expr();
233233
program.assign(stashed_sym.symbol_expr(), orig.symbol_expr());

src/goto-instrument/accelerate/polynomial_accelerator.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -768,7 +768,7 @@ void polynomial_acceleratort::stash_variables(
768768
it!=vars.end();
769769
++it)
770770
{
771-
symbolt orig=*symbol_table.lookup(*it);
771+
const symbolt &orig = symbol_table.lookup_ref(*it);
772772
symbolt stashed_sym=utils.fresh_symbol("polynomial::stash", orig.type);
773773
substitution[orig.symbol_expr()]=stashed_sym.symbol_expr();
774774
program.assign(stashed_sym.symbol_expr(), orig.symbol_expr());

src/goto-instrument/dump_c.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -89,7 +89,7 @@ void dump_ct::operator()(std::ostream &os)
8989
std::set<std::string> symbols_sorted;
9090
for(const auto &named_symbol : copied_symbol_table.symbols)
9191
{
92-
symbolt &symbol=*copied_symbol_table.get_writeable(named_symbol.first);
92+
symbolt &symbol = copied_symbol_table.get_writeable_ref(named_symbol.first);
9393
bool tag_added=false;
9494

9595
// TODO we could get rid of some of the ID_anonymous by looking up

src/goto-instrument/goto_program2code.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1630,7 +1630,7 @@ void goto_program2codet::remove_const(typet &type)
16301630
if(!const_removed.insert(identifier).second)
16311631
return;
16321632

1633-
symbolt &symbol=*symbol_table.get_writeable(identifier);
1633+
symbolt &symbol = symbol_table.get_writeable_ref(identifier);
16341634
INVARIANT(
16351635
symbol.is_type,
16361636
"Symbol "+id2string(identifier)+" should be a type");

src/goto-programs/rebuild_goto_start_function.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -76,8 +76,8 @@ template<typename maybe_lazy_goto_modelt>
7676
irep_idt rebuild_goto_start_function_baset<maybe_lazy_goto_modelt>::
7777
get_entry_point_mode() const
7878
{
79-
const symbolt &current_entry_point=
80-
*goto_model.symbol_table.lookup(goto_functionst::entry_point());
79+
const symbolt &current_entry_point =
80+
goto_model.symbol_table.lookup_ref(goto_functionst::entry_point());
8181
return current_entry_point.mode;
8282
}
8383

src/goto-programs/remove_complex.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -276,7 +276,7 @@ static void remove_complex(symbolt &symbol)
276276
void remove_complex(symbol_tablet &symbol_table)
277277
{
278278
for(const auto &named_symbol : symbol_table.symbols)
279-
remove_complex(*symbol_table.get_writeable(named_symbol.first));
279+
remove_complex(symbol_table.get_writeable_ref(named_symbol.first));
280280
}
281281

282282
/// removes complex data type

src/goto-programs/remove_const_function_pointers.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ exprt remove_const_function_pointerst::replace_const_symbols(
7575
if(is_const_expression(expression))
7676
{
7777
const symbolt &symbol =
78-
*symbol_table.lookup(to_symbol_expr(expression).get_identifier());
78+
symbol_table.lookup_ref(to_symbol_expr(expression).get_identifier());
7979
if(symbol.type.id()!=ID_code)
8080
{
8181
const exprt &symbol_value=symbol.value;
@@ -111,8 +111,7 @@ exprt remove_const_function_pointerst::replace_const_symbols(
111111
exprt remove_const_function_pointerst::resolve_symbol(
112112
const symbol_exprt &symbol_expr) const
113113
{
114-
const symbolt &symbol=
115-
*symbol_table.lookup(symbol_expr.get_identifier());
114+
const symbolt &symbol = symbol_table.lookup_ref(symbol_expr.get_identifier());
116115
return symbol.value;
117116
}
118117

src/goto-programs/remove_vector.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -211,7 +211,7 @@ static void remove_vector(symbolt &symbol)
211211
static void remove_vector(symbol_tablet &symbol_table)
212212
{
213213
for(const auto &named_symbol : symbol_table.symbols)
214-
remove_vector(*symbol_table.get_writeable(named_symbol.first));
214+
remove_vector(symbol_table.get_writeable_ref(named_symbol.first));
215215
}
216216

217217
/// removes vector data type

src/goto-programs/string_abstraction.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -163,7 +163,7 @@ void string_abstractiont::add_str_arguments(
163163
const irep_idt &name,
164164
goto_functionst::goto_functiont &fct)
165165
{
166-
symbolt &fct_symbol=*symbol_table.get_writeable(name);
166+
symbolt &fct_symbol = symbol_table.get_writeable_ref(name);
167167

168168
code_typet::parameterst str_args;
169169

src/jsil/jsil_typecheck.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -897,15 +897,15 @@ void jsil_typecheckt::typecheck()
897897
// recursively doing base classes first.
898898
for(const irep_idt &id : identifiers)
899899
{
900-
symbolt &symbol=*symbol_table.get_writeable(id);
900+
symbolt &symbol = symbol_table.get_writeable_ref(id);
901901
if(symbol.is_type)
902902
typecheck_type_symbol(symbol);
903903
}
904904

905905
// We now check all non-type symbols
906906
for(const irep_idt &id : identifiers)
907907
{
908-
symbolt &symbol=*symbol_table.get_writeable(id);
908+
symbolt &symbol = symbol_table.get_writeable_ref(id);
909909
if(!symbol.is_type)
910910
typecheck_non_type_symbol(symbol);
911911
}

src/linking/linking.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1309,7 +1309,7 @@ void linkingt::rename_symbols(
13091309

13101310
for(const irep_idt &id : needs_to_be_renamed)
13111311
{
1312-
symbolt &new_symbol=*src_symbol_table.get_writeable(id);
1312+
symbolt &new_symbol = src_symbol_table.get_writeable_ref(id);
13131313

13141314
irep_idt new_identifier;
13151315

@@ -1372,7 +1372,7 @@ void linkingt::copy_symbols()
13721372
// Now do the collisions
13731373
for(const irep_idt &collision : collisions)
13741374
{
1375-
symbolt &old_symbol=*main_symbol_table.get_writeable(collision);
1375+
symbolt &old_symbol = main_symbol_table.get_writeable_ref(collision);
13761376
symbolt &new_symbol=src_symbols.at(collision);
13771377

13781378
if(new_symbol.is_type)

src/linking/static_lifetime_init.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,7 @@ static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
5757
{
5858
// C standard 6.9.2, paragraph 5
5959
// adjust the type to an array of size 1
60-
symbolt &writable_symbol = *symbol_table.get_writeable(identifier);
60+
symbolt &writable_symbol = symbol_table.get_writeable_ref(identifier);
6161
writable_symbol.type = type;
6262
writable_symbol.type.set(ID_size, from_integer(1, size_type()));
6363
}

src/pointer-analysis/add_failed_symbols.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,7 @@ void add_failed_symbol_if_needed(
6767
if(symbol.type.get(ID_C_failed_symbol)!="")
6868
return;
6969

70-
add_failed_symbol(*symbol_table.get_writeable(symbol.name), symbol_table);
70+
add_failed_symbol(symbol_table.get_writeable_ref(symbol.name), symbol_table);
7171
}
7272

7373
/// Create a failed-dereference symbol for all symbols in the given table that

0 commit comments

Comments
 (0)