Modify/add symbol table lookup and get_writeable

reuk · reuk · commit a9ba0f90aa18 · 2017-10-11T12:11:12.000+01:00
diff --git a/CODING_STANDARD.md b/CODING_STANDARD.md
@@ -182,6 +182,11 @@ Here a few minimalistic coding rules for the CPROVER source tree.
 - Avoid `assert`. If the condition is an actual invariant, use INVARIANT,
   PRECONDITION, POSTCONDITION, CHECK_RETURN, UNREACHABLE or DATA_INVARIANT. If
   there are possible reasons why it might fail, throw an exception.
+- All raw pointers (such as those returned by `symbol_tablet::lookup`) are
+  assumed to be non-owning, and should not be `delete`d. Raw pointers that
+  point to heap-allocated memory should be private data members of an object
+  which safely manages the pointer. As such, `new` should only be used in
+  constructors, and `delete` in destructors. Never use `malloc` or `free`.
 
 # Architecture-specific code
 - Avoid if possible.
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
@@ -208,7 +208,7 @@ void c_typecheck_baset::typecheck_type(typet &type)
       {
         const irep_idt &tag_name=
           to_c_enum_tag_type(type.subtype()).get_identifier();
-        symbol_table.get_writeable(tag_name)->get().type.subtype()=result;
+        symbol_table.get_writeable_ref(tag_name).type.subtype()=result;
       }
 
       type=result;
@@ -782,7 +782,7 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
           type.set(ID_tag, base_name);
 
           typecheck_compound_body(type);
-          symbol_table.get_writeable(s_it->first)->get().type.swap(type);
+          symbol_table.get_writeable_ref(s_it->first).type.swap(type);
         }
       }
       else if(have_body)
@@ -1220,7 +1220,7 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
     {
       // Ok, overwrite the type in the symbol table.
       // This gives us the members and the subtype.
-      symbol_table.get_writeable(symbol.name)->get().type=enum_tag_symbol.type;
+      symbol_table.get_writeable_ref(symbol.name).type=enum_tag_symbol.type;
     }
     else if(symbol.type.id()==ID_c_enum)
     {
diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp
@@ -98,7 +98,7 @@ symbolt &cpp_declarator_convertert::convert(
     }
 
     // try static first
-    symbol_tablet::opt_symbol_reft maybe_symbol=
+    auto maybe_symbol=
       cpp_typecheck.symbol_table.get_writeable(final_identifier);
 
     if(!maybe_symbol)
@@ -191,7 +191,7 @@ symbolt &cpp_declarator_convertert::convert(
     }
 
     // already there?
-    symbol_tablet::opt_symbol_reft maybe_symbol=
+    const auto maybe_symbol=
       cpp_typecheck.symbol_table.get_writeable(final_identifier);
     if(!maybe_symbol)
       return convert_new_symbol(storage_spec, member_spec, declarator);
diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp
@@ -178,7 +178,7 @@ void cpp_typecheckt::static_and_dynamic_initialization()
 
       // Make it nil to get zero initialization by
       // __CPROVER_initialize
-      symbol_table.get_writeable(d_it)->get().value.make_nil();
+      symbol_table.get_writeable_ref(d_it).value.make_nil();
     }
     else
     {
@@ -260,7 +260,7 @@ void cpp_typecheckt::do_not_typechecked()
   for(const auto &named_symbol : symbol_table.symbols)
   {
     if(named_symbol.second.value.id()=="cpp_not_typechecked")
-      symbol_table.get_writeable(named_symbol.first)->get().value.make_nil();
+      symbol_table.get_writeable_ref(named_symbol.first).value.make_nil();
   }
 }
 
@@ -286,7 +286,7 @@ void cpp_typecheckt::clean_up()
     {
       // remove methods from 'components'
       struct_union_typet &struct_union_type=to_struct_union_type(
-        symbol_table.get_writeable(cur_it->first)->get().type);
+        symbol_table.get_writeable_ref(cur_it->first).type);
 
       const struct_union_typet::componentst &components=
         struct_union_type.components();
diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp
@@ -159,9 +159,7 @@ void cpp_typecheckt::typecheck_compound_type(
 
   // check if we have it already
 
-  symbol_tablet::opt_const_symbol_reft maybe_symbol=
-    symbol_table.lookup(symbol_name);
-  if(maybe_symbol)
+  if(const auto maybe_symbol=symbol_table.lookup(symbol_name))
   {
     // we do!
     const symbolt &symbol=*maybe_symbol;
@@ -553,7 +551,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
         put_compound_into_scope(compo);
       }
 
-      typet &vt=symbol_table.get_writeable(vt_name)->get().type;
+      typet &vt=symbol_table.get_writeable_ref(vt_name).type;
       INVARIANT(vt.id()==ID_struct, "Virtual tables must be stored as struct");
       struct_typet &virtual_table=to_struct_type(vt);
 
diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp
@@ -105,7 +105,7 @@ void cpp_typecheckt::convert_anonymous_union(
     id.is_member=true;
   }
 
-  symbol_table.get_writeable(union_symbol.name)->get().type.set(
+  symbol_table.get_writeable_ref(union_symbol.name).type.set(
     "#unnamed_object", symbol.base_name);
 
   code.swap(new_code);
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
@@ -1244,8 +1244,7 @@ void cpp_typecheckt::typecheck_expr_member(
     assert(it!=symbol_table.symbols.end());
 
     if(it->second.value.id()=="cpp_not_typechecked")
-      symbol_table.get_writeable(component_name)->get()
-        .value.set("is_used", true);
+      symbol_table.get_writeable_ref(component_name).value.set("is_used", true);
   }
 }
 
@@ -2203,7 +2202,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
            type.id()==ID_code &&
            type.find(ID_return_type).id()==ID_destructor)
         {
-          add_method_body(&symbol_table.get_writeable(it->get(ID_name))->get());
+          add_method_body(&symbol_table.get_writeable_ref(it->get(ID_name)));
           break;
         }
       }
@@ -2372,7 +2371,7 @@ void cpp_typecheckt::typecheck_method_application(
   member_expr.swap(expr.function());
 
   const symbolt &symbol=lookup(member_expr.get(ID_component_name));
-  add_method_body(&symbol_table.get_writeable(symbol.name)->get());
+  add_method_body(&symbol_table.get_writeable_ref(symbol.name));
 
   // build new function expression
   exprt new_function(cpp_symbol_expr(symbol));
@@ -2414,7 +2413,7 @@ void cpp_typecheckt::typecheck_method_application(
   if(symbol.value.id()=="cpp_not_typechecked" &&
      !symbol.value.get_bool("is_used"))
   {
-    symbol_table.get_writeable(symbol.name)->get().value.set("is_used", true);
+    symbol_table.get_writeable_ref(symbol.name).value.set("is_used", true);
   }
 }
 
@@ -2683,7 +2682,7 @@ void cpp_typecheckt::typecheck_expr_function_identifier(exprt &expr)
     assert(it != symbol_table.symbols.end());
 
     if(it->second.value.id()=="cpp_not_typechecked")
-      symbol_table.get_writeable(it->first)->get().value.set("is_used", true);
+      symbol_table.get_writeable_ref(it->first).value.set("is_used", true);
   }
 
   c_typecheck_baset::typecheck_expr_function_identifier(expr);
diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp
@@ -107,9 +107,7 @@ void cpp_typecheckt::typecheck_class_template(
 
   // check if we have it already
 
-  symbol_tablet::opt_symbol_reft maybe_symbol=
-    symbol_table.get_writeable(symbol_name);
-  if(maybe_symbol)
+  if(const auto maybe_symbol=symbol_table.get_writeable(symbol_name))
   {
     // there already
     symbolt &previous_symbol=*maybe_symbol;
@@ -265,7 +263,7 @@ void cpp_typecheckt::typecheck_function_template(
 
     if(has_value)
     {
-      symbol_table.get_writeable(symbol_name)->get().type.swap(declaration);
+      symbol_table.get_writeable_ref(symbol_name).type.swap(declaration);
       cpp_scopes.id_map[symbol_name]=&template_scope;
     }
 
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
@@ -725,7 +725,7 @@ void compilet::convert_symbols(goto_functionst &dest)
       {
         debug() << "Compiling " << s_it->first << eom;
         converter.convert_function(s_it->first);
-        symbol_table.get_writeable(*it)->get().value=exprt("compiled");
+        symbol_table.get_writeable_ref(*it).value=exprt("compiled");
       }
     }
   }
diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp
@@ -168,8 +168,7 @@ int linker_script_merget::pointerize_linker_defined_symbols(
   // First, pointerize the actual linker-defined symbols
   for(const auto &pair : linker_values)
   {
-    symbol_tablet::opt_symbol_reft maybe_symbol=
-      symbol_table.get_writeable(pair.first);
+    const auto maybe_symbol=symbol_table.get_writeable(pair.first);
     if(!maybe_symbol)
       continue;
     symbolt &entry=*maybe_symbol;
@@ -190,7 +189,7 @@ int linker_script_merget::pointerize_linker_defined_symbols(
     debug() << "Pointerizing the symbol-table value of symbol " << pair.first
             << eom;
     int fail=pointerize_subexprs_of(
-      symbol_table.get_writeable(pair.first)->get().value,
+      symbol_table.get_writeable_ref(pair.first).value,
       to_pointerize,
       linker_values);
     if(to_pointerize.empty() && fail==0)
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
@@ -55,7 +55,7 @@ void dump_ct::operator()(std::ostream &os)
       continue;
 
     code_typet &code_type=to_code_type(
-      copied_symbol_table.get_writeable(named_symbol.first)->get().type);
+      copied_symbol_table.get_writeable_ref(named_symbol.first).type);
     code_typet::parameterst &parameters=code_type.parameters();
 
     for(code_typet::parameterst::iterator
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
@@ -134,7 +134,7 @@ void goto_program2codet::scan_for_varargs()
     system_headers.insert("stdarg.h");
 
     code_typet &code_type=
-      to_code_type(symbol_table.get_writeable(func_name)->get().type);
+      to_code_type(symbol_table.get_writeable_ref(func_name).type);
     code_typet::parameterst &parameters=code_type.parameters();
 
     for(code_typet::parameterst::iterator
diff --git a/src/goto-instrument/remove_function.cpp b/src/goto-instrument/remove_function.cpp
@@ -51,7 +51,7 @@ void remove_function(
     message.status() << "Removing body of " << identifier
                      << messaget::eom;
     entry->second.clear();
-    goto_model.symbol_table.get_writeable(identifier)->get().value.make_nil();
+    goto_model.symbol_table.get_writeable_ref(identifier).value.make_nil();
   }
 }
 
diff --git a/src/goto-instrument/wmm/shared_buffers.h b/src/goto-instrument/wmm/shared_buffers.h
@@ -158,11 +158,10 @@ class shared_bufferst
 
   irep_idt choice(const irep_idt &function, const std::string &suffix)
   {
-    symbol_tablet::opt_const_symbol_reft maybe_symbol=
-      symbol_table.lookup(function);
+    const auto maybe_symbol=symbol_table.lookup(function);
     const std::string function_base_name =
       maybe_symbol
-        ? id2string(maybe_symbol->get().base_name)
+        ? id2string(maybe_symbol->base_name)
         : "main";
     return add(function_base_name+"_weak_choice",
       function_base_name+"_weak_choice", suffix, bool_typet());
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
@@ -444,7 +444,7 @@ typet interpretert::get_type(const irep_idt &id) const
 {
   dynamic_typest::const_iterator it=dynamic_types.find(id);
   if(it==dynamic_types.end())
-    return symbol_table.lookup(id)->get().type;
+    return symbol_table.lookup_ref(id).type;
   return it->second;
 }
 
@@ -1041,7 +1041,7 @@ exprt interpretert::get_value(const irep_idt &id)
   if(findit!=dynamic_types.end())
     get_type=findit->second;
   else
-    get_type=symbol_table.lookup(id)->get().type;
+    get_type=symbol_table.lookup_ref(id).type;
 
   symbol_exprt symbol_expr(id, get_type);
   mp_integer whole_lhs_object_address=evaluate_address(symbol_expr);
diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp
@@ -118,13 +118,13 @@ void mm_io(
   irep_idt id_r=CPROVER_PREFIX "mm_io_r";
   irep_idt id_w=CPROVER_PREFIX "mm_io_w";
 
-  symbol_tablet::opt_const_symbol_reft maybe_symbol=symbol_table.lookup(id_r);
+  auto maybe_symbol=symbol_table.lookup(id_r);
   if(maybe_symbol)
-    mm_io_r=maybe_symbol->get().symbol_expr();
+    mm_io_r=maybe_symbol->symbol_expr();
 
   maybe_symbol=symbol_table.lookup(id_w);
   if(maybe_symbol)
-    mm_io_w=maybe_symbol->get().symbol_expr();
+    mm_io_w=maybe_symbol->symbol_expr();
 
   for(auto & f : goto_functions.function_map)
     mm_io(mm_io_r, mm_io_w, f.second, ns);
diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp
@@ -134,8 +134,7 @@ void remove_exceptionst::add_exceptional_returns(
   const irep_idt &function_id=func_it->first;
   goto_programt &goto_program=func_it->second.body;
 
-  symbol_tablet::opt_const_symbol_reft maybe_symbol=
-    symbol_table.lookup(function_id);
+  auto maybe_symbol=symbol_table.lookup(function_id);
   INVARIANT(maybe_symbol, "functions should be recorded in the symbol table");
   const symbolt &function_symbol=*maybe_symbol;
 
@@ -255,11 +254,9 @@ void remove_exceptionst::instrument_exception_handler(
     to_code_landingpad(instr_it->code).catch_expr();
   irep_idt thrown_exception_global=id2string(function_id)+EXC_SUFFIX;
 
-  symbol_tablet::opt_const_symbol_reft maybe_symbol=
-    symbol_table.lookup(thrown_exception_global);
-  if(maybe_symbol)
+  if(const auto maybe_symbol=symbol_table.lookup(thrown_exception_global))
   {
-    const symbol_exprt thrown_global_symbol=maybe_symbol->get().symbol_expr();
+    const symbol_exprt thrown_global_symbol=maybe_symbol->symbol_expr();
     // next we reset the exceptional return to NULL
     null_pointer_exprt null_voidptr((pointer_type(empty_typet())));
 
@@ -425,9 +422,9 @@ void remove_exceptionst::instrument_function_call(
   const irep_idt &callee_id=
     to_symbol_expr(function_call.function()).get_identifier();
 
-  symbol_tablet::opt_const_symbol_reft callee_inflight_exception=
+  const auto callee_inflight_exception=
     symbol_table.lookup(id2string(callee_id)+EXC_SUFFIX);
-  symbol_tablet::opt_const_symbol_reft local_inflight_exception=
+  const auto local_inflight_exception=
     symbol_table.lookup(id2string(function_id)+EXC_SUFFIX);
 
   if(callee_inflight_exception && local_inflight_exception)
@@ -436,9 +433,9 @@ void remove_exceptionst::instrument_function_call(
       func_it, instr_it, stack_catch, locals);
 
     const symbol_exprt callee_inflight_exception_expr=
-      callee_inflight_exception->get().symbol_expr();
+      callee_inflight_exception->symbol_expr();
     const symbol_exprt local_inflight_exception_expr=
-      local_inflight_exception->get().symbol_expr();
+      local_inflight_exception->symbol_expr();
 
     // add a null check (so that instanceof can be applied)
     equal_exprt eq_null(
diff --git a/src/goto-programs/remove_static_init_loops.cpp b/src/goto-programs/remove_static_init_loops.cpp
@@ -58,8 +58,7 @@ void remove_static_init_loopst::unwind_enum_static(
         const std::string &fname=id2string(ins.function);
         size_t class_prefix_length=fname.find_last_of('.');
         // is the function symbol in the symbol table?
-        symbol_tablet::opt_const_symbol_reft maybe_symbol=
-          symbol_table.lookup(ins.function);
+        const auto maybe_symbol=symbol_table.lookup(ins.function);
         if(!maybe_symbol)
         {
           message.warning() << "function `" << id2string(ins.function)
diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp
@@ -144,7 +144,7 @@ bool ci_lazy_methodst::operator()(
         method_converter(
           *parsed_method.first, *parsed_method.second, new_lazy_methods);
         gather_virtual_callsites(
-          symbol_table.lookup(mname)->get().value,
+          symbol_table.lookup_ref(mname).value,
           virtual_callsites);
         any_new_methods=true;
       }
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -893,8 +893,7 @@ bool java_bytecode_convert_methodt::class_needs_clinit(
     findit_any.first->second=true;
     return true;
   }
-  symbol_tablet::opt_const_symbol_reft maybe_symbol=
-    symbol_table.lookup(classname);
+  const auto maybe_symbol=symbol_table.lookup(classname);
   // Stub class?
   if(!maybe_symbol)
   {
diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp
@@ -617,5 +617,5 @@ void java_bytecode_instrument(
   // instrument(...) can add symbols to the table, so it's
   // not safe to hold a reference to a symbol across a call.
   for(const auto &symbol : symbols_to_instrument)
-    instrument(symbol_table.get_writeable(symbol)->get().value);
+    instrument(symbol_table.get_writeable_ref(symbol).value);
 }
diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp
diff --git a/src/jsil/jsil_convert.cpp b/src/jsil/jsil_convert.cpp
diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp
diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp
diff --git a/src/util/config.cpp b/src/util/config.cpp
diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp
diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h
diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp
diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp

Original file line number	Diff line number	Diff line change
`@@ -208,7 +208,7 @@ void c_typecheck_baset::typecheck_type(typet &type)`
`208`	`208`	`{`
`209`	`209`	`const irep_idt &tag_name=`
`210`	`210`	`to_c_enum_tag_type(type.subtype()).get_identifier();`
`211`		`- symbol_table.get_writeable(tag_name)->get().type.subtype()=result;`
	`211`	`+ symbol_table.get_writeable_ref(tag_name).type.subtype()=result;`
`212`	`212`	`}`
`213`	`213`
`214`	`214`	`type=result;`
`@@ -782,7 +782,7 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)`
`782`	`782`	`type.set(ID_tag, base_name);`
`783`	`783`
`784`	`784`	`typecheck_compound_body(type);`
`785`		`- symbol_table.get_writeable(s_it->first)->get().type.swap(type);`
	`785`	`+ symbol_table.get_writeable_ref(s_it->first).type.swap(type);`
`786`	`786`	`}`
`787`	`787`	`}`
`788`	`788`	`else if(have_body)`
`@@ -1220,7 +1220,7 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)`
`1220`	`1220`	`{`
`1221`	`1221`	`// Ok, overwrite the type in the symbol table.`
`1222`	`1222`	`// This gives us the members and the subtype.`
`1223`		`- symbol_table.get_writeable(symbol.name)->get().type=enum_tag_symbol.type;`
	`1223`	`+ symbol_table.get_writeable_ref(symbol.name).type=enum_tag_symbol.type;`
`1224`	`1224`	`}`
`1225`	`1225`	`else if(symbol.type.id()==ID_c_enum)`
`1226`	`1226`	`{`
Original file line number	Diff line number	Diff line change
`@@ -98,7 +98,7 @@ symbolt &cpp_declarator_convertert::convert(`
`98`	`98`	`}`
`99`	`99`
`100`	`100`	`// try static first`
`101`		`- symbol_tablet::opt_symbol_reft maybe_symbol=`
	`101`	`+ auto maybe_symbol=`
`102`	`102`	`cpp_typecheck.symbol_table.get_writeable(final_identifier);`
`103`	`103`
`104`	`104`	`if(!maybe_symbol)`
`@@ -191,7 +191,7 @@ symbolt &cpp_declarator_convertert::convert(`
`191`	`191`	`}`
`192`	`192`
`193`	`193`	`// already there?`
`194`		`- symbol_tablet::opt_symbol_reft maybe_symbol=`
	`194`	`+ const auto maybe_symbol=`
`195`	`195`	`cpp_typecheck.symbol_table.get_writeable(final_identifier);`
`196`	`196`	`if(!maybe_symbol)`
`197`	`197`	`return convert_new_symbol(storage_spec, member_spec, declarator);`
Original file line number	Diff line number	Diff line change
`@@ -178,7 +178,7 @@ void cpp_typecheckt::static_and_dynamic_initialization()`
`178`	`178`
`179`	`179`	`// Make it nil to get zero initialization by`
`180`	`180`	`// __CPROVER_initialize`
`181`		`- symbol_table.get_writeable(d_it)->get().value.make_nil();`
	`181`	`+ symbol_table.get_writeable_ref(d_it).value.make_nil();`
`182`	`182`	`}`
`183`	`183`	`else`
`184`	`184`	`{`
`@@ -260,7 +260,7 @@ void cpp_typecheckt::do_not_typechecked()`
`260`	`260`	`for(const auto &named_symbol : symbol_table.symbols)`
`261`	`261`	`{`
`262`	`262`	`if(named_symbol.second.value.id()=="cpp_not_typechecked")`
`263`		`- symbol_table.get_writeable(named_symbol.first)->get().value.make_nil();`
	`263`	`+ symbol_table.get_writeable_ref(named_symbol.first).value.make_nil();`
`264`	`264`	`}`
`265`	`265`	`}`
`266`	`266`
`@@ -286,7 +286,7 @@ void cpp_typecheckt::clean_up()`
`286`	`286`	`{`
`287`	`287`	`// remove methods from 'components'`
`288`	`288`	`struct_union_typet &struct_union_type=to_struct_union_type(`
`289`		`- symbol_table.get_writeable(cur_it->first)->get().type);`
	`289`	`+ symbol_table.get_writeable_ref(cur_it->first).type);`
`290`	`290`
`291`	`291`	`const struct_union_typet::componentst &components=`
`292`	`292`	`struct_union_type.components();`
Original file line number	Diff line number	Diff line change
`@@ -105,7 +105,7 @@ void cpp_typecheckt::convert_anonymous_union(`
`105`	`105`	`id.is_member=true;`
`106`	`106`	`}`
`107`	`107`
`108`		`- symbol_table.get_writeable(union_symbol.name)->get().type.set(`
	`108`	`+ symbol_table.get_writeable_ref(union_symbol.name).type.set(`
`109`	`109`	`"#unnamed_object", symbol.base_name);`
`110`	`110`
`111`	`111`	`code.swap(new_code);`
Original file line number	Diff line number	Diff line change
`@@ -1244,8 +1244,7 @@ void cpp_typecheckt::typecheck_expr_member(`
`1244`	`1244`	`assert(it!=symbol_table.symbols.end());`
`1245`	`1245`
`1246`	`1246`	`if(it->second.value.id()=="cpp_not_typechecked")`
`1247`		`- symbol_table.get_writeable(component_name)->get()`
`1248`		`- .value.set("is_used", true);`
	`1247`	`+ symbol_table.get_writeable_ref(component_name).value.set("is_used", true);`
`1249`	`1248`	`}`
`1250`	`1249`	`}`
`1251`	`1250`
`@@ -2203,7 +2202,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call(`
`2203`	`2202`	`type.id()==ID_code &&`
`2204`	`2203`	`type.find(ID_return_type).id()==ID_destructor)`
`2205`	`2204`	`{`
`2206`		`- add_method_body(&symbol_table.get_writeable(it->get(ID_name))->get());`
	`2205`	`+ add_method_body(&symbol_table.get_writeable_ref(it->get(ID_name)));`
`2207`	`2206`	`break;`
`2208`	`2207`	`}`
`2209`	`2208`	`}`
`@@ -2372,7 +2371,7 @@ void cpp_typecheckt::typecheck_method_application(`
`2372`	`2371`	`member_expr.swap(expr.function());`
`2373`	`2372`
`2374`	`2373`	`const symbolt &symbol=lookup(member_expr.get(ID_component_name));`
`2375`		`- add_method_body(&symbol_table.get_writeable(symbol.name)->get());`
	`2374`	`+ add_method_body(&symbol_table.get_writeable_ref(symbol.name));`
`2376`	`2375`
`2377`	`2376`	`// build new function expression`
`2378`	`2377`	`exprt new_function(cpp_symbol_expr(symbol));`
`@@ -2414,7 +2413,7 @@ void cpp_typecheckt::typecheck_method_application(`
`2414`	`2413`	`if(symbol.value.id()=="cpp_not_typechecked" &&`
`2415`	`2414`	`!symbol.value.get_bool("is_used"))`
`2416`	`2415`	`{`
`2417`		`- symbol_table.get_writeable(symbol.name)->get().value.set("is_used", true);`
	`2416`	`+ symbol_table.get_writeable_ref(symbol.name).value.set("is_used", true);`
`2418`	`2417`	`}`
`2419`	`2418`	`}`
`2420`	`2419`
`@@ -2683,7 +2682,7 @@ void cpp_typecheckt::typecheck_expr_function_identifier(exprt &expr)`
`2683`	`2682`	`assert(it != symbol_table.symbols.end());`
`2684`	`2683`
`2685`	`2684`	`if(it->second.value.id()=="cpp_not_typechecked")`
`2686`		`- symbol_table.get_writeable(it->first)->get().value.set("is_used", true);`
	`2685`	`+ symbol_table.get_writeable_ref(it->first).value.set("is_used", true);`
`2687`	`2686`	`}`
`2688`	`2687`
`2689`	`2688`	`c_typecheck_baset::typecheck_expr_function_identifier(expr);`
Original file line number	Diff line number	Diff line change
`@@ -107,9 +107,7 @@ void cpp_typecheckt::typecheck_class_template(`
`107`	`107`
`108`	`108`	`// check if we have it already`
`109`	`109`
`110`		`- symbol_tablet::opt_symbol_reft maybe_symbol=`
`111`		`- symbol_table.get_writeable(symbol_name);`
`112`		`- if(maybe_symbol)`
	`110`	`+ if(const auto maybe_symbol=symbol_table.get_writeable(symbol_name))`
`113`	`111`	`{`
`114`	`112`	`// there already`
`115`	`113`	`symbolt &previous_symbol=*maybe_symbol;`
`@@ -265,7 +263,7 @@ void cpp_typecheckt::typecheck_function_template(`
`265`	`263`
`266`	`264`	`if(has_value)`
`267`	`265`	`{`
`268`		`- symbol_table.get_writeable(symbol_name)->get().type.swap(declaration);`
	`266`	`+ symbol_table.get_writeable_ref(symbol_name).type.swap(declaration);`
`269`	`267`	`cpp_scopes.id_map[symbol_name]=&template_scope;`
`270`	`268`	`}`
`271`	`269`
Original file line number	Diff line number	Diff line change
`@@ -725,7 +725,7 @@ void compilet::convert_symbols(goto_functionst &dest)`
`725`	`725`	`{`
`726`	`726`	`debug() << "Compiling " << s_it->first << eom;`
`727`	`727`	`converter.convert_function(s_it->first);`
`728`		`- symbol_table.get_writeable(*it)->get().value=exprt("compiled");`
	`728`	`+ symbol_table.get_writeable_ref(*it).value=exprt("compiled");`
`729`	`729`	`}`
`730`	`730`	`}`
`731`	`731`	`}`