@@ -319,7 +319,9 @@ void smv_typecheckt::instantiate(
319
319
320
320
std::set<irep_idt> var_identifiers;
321
321
322
- forall_symbol_module_map (v_it, symbol_table.symbol_module_map , identifier)
322
+ for (auto v_it=symbol_table.symbol_module_map .lower_bound (identifier);
323
+ v_it!=symbol_table.symbol_module_map .upper_bound (identifier);
324
+ v_it++)
323
325
{
324
326
symbol_tablet::symbolst::const_iterator s_it2=
325
327
symbol_table.symbols .find (v_it->second );
@@ -360,16 +362,16 @@ void smv_typecheckt::instantiate(
360
362
v_it!=var_identifiers.end ();
361
363
v_it++)
362
364
{
363
- symbol_tablet::symbolst::iterator s_it2=
364
- symbol_table.symbols . find (*v_it);
365
+ auto s_it2=
366
+ symbol_table.get_writeable (*v_it);
365
367
366
- if (s_it2==symbol_table. symbols . end () )
368
+ if (s_it2==nullptr )
367
369
{
368
370
error () << " symbol `" << *v_it << " ' not found" << eom;
369
371
throw 0 ;
370
372
}
371
373
372
- symbolt &symbol=s_it2-> second ;
374
+ symbolt &symbol=* s_it2;
373
375
374
376
if (!symbol.value .is_nil ())
375
377
{
@@ -632,16 +634,16 @@ void smv_typecheckt::typecheck(
632
634
if (define_map.find (identifier)!=define_map.end ())
633
635
convert_define (identifier);
634
636
635
- symbol_tablet::symbolst::iterator s_it=symbol_table.symbols . find (identifier);
637
+ auto s_it=symbol_table.get_writeable (identifier);
636
638
637
- if (s_it==symbol_table. symbols . end () )
639
+ if (s_it==nullptr )
638
640
{
639
641
error ().source_location =expr.find_source_location ();
640
642
error () << " variable `" << identifier << " ' not found" << eom;
641
643
throw 0 ;
642
644
}
643
645
644
- symbolt &symbol=s_it-> second ;
646
+ symbolt &symbol=* s_it;
645
647
646
648
assert (symbol.type .is_not_nil ());
647
649
expr.type ()=symbol.type ;
@@ -1253,16 +1255,16 @@ void smv_typecheckt::collect_define(const exprt &expr)
1253
1255
1254
1256
const irep_idt &identifier=op0.get (ID_identifier);
1255
1257
1256
- symbol_tablet::symbolst::iterator it=symbol_table.symbols . find (identifier);
1258
+ auto it=symbol_table.get_writeable (identifier);
1257
1259
1258
- if (it==symbol_table. symbols . end () )
1260
+ if (it==nullptr )
1259
1261
{
1260
1262
error () << " collect_define failed to find symbol `"
1261
1263
<< identifier << " '" << eom;
1262
1264
throw 0 ;
1263
1265
}
1264
1266
1265
- symbolt &symbol=it-> second ;
1267
+ symbolt &symbol=*it ;
1266
1268
1267
1269
symbol.value .make_nil ();
1268
1270
symbol.is_input =false ;
@@ -1304,16 +1306,16 @@ void smv_typecheckt::convert_define(const irep_idt &identifier)
1304
1306
throw 0 ;
1305
1307
}
1306
1308
1307
- symbol_tablet::symbolst::iterator it=symbol_table.symbols . find (identifier);
1309
+ auto it=symbol_table.get_writeable (identifier);
1308
1310
1309
- if (it==symbol_table. symbols . end () )
1311
+ if (it==nullptr )
1310
1312
{
1311
1313
error () << " convert_define failed to find symbol `"
1312
1314
<< identifier << " '" << eom;
1313
1315
throw 0 ;
1314
1316
}
1315
1317
1316
- symbolt &symbol=it-> second ;
1318
+ symbolt &symbol=*it ;
1317
1319
1318
1320
d.in_progress =true ;
1319
1321
0 commit comments