goto-instrument: use new symbolt constructors

To the extent possible, apply resource-acquisition-is-initialisation.
The constructors ensure that at least the most essential fields (name,
type, mode) are set.

Author: tautschnig

regression/goto-instrument/dump-type-header-exclude-non-module-var/main.c

@@ -8,11 +8,13 @@ struct B
 
 #define temperature(x) x.t
 
+int __VERIFIER_nondet_int();
+
 int main()
 {
   struct B aStruct = {3, 8};
   __CPROVER_assert(my_config.a == 7, "Should be valid");
-  my_config.a = nondet_int();
+  my_config.a = __VERIFIER_nondet_int();
 
   __CPROVER_assert(!(my_config.a == 4), "Should be nondet now");
   __CPROVER_assert(aStruct.t, "Should not be null");

src/goto-instrument/accelerate/accelerate.cpp

@@ -435,12 +435,10 @@ bool acceleratet::is_underapproximate(path_acceleratort &accelerator)
 
 symbolt acceleratet::make_symbol(std::string name, typet type)
 {
-  symbolt ret;
+  symbolt ret{name, std::move(type), irep_idt{}};
   ret.module="accelerate";
-  ret.name=name;
   ret.base_name=name;
   ret.pretty_name=name;
-  ret.type=type;
 
   symbol_table.add(ret);
 

src/goto-instrument/accelerate/acceleration_utils.cpp

@@ -1250,12 +1250,10 @@ symbolt acceleration_utilst::fresh_symbol(std::string base, typet type)
   static int num_symbols=0;
 
   std::string name=base + "_" + std::to_string(num_symbols++);
-  symbolt ret;
+  symbolt ret{name, std::move(type), irep_idt{}};
   ret.module="scratch";
-  ret.name=name;
   ret.base_name=name;
   ret.pretty_name=name;
-  ret.type=type;
 
   symbol_table.add(ret);
 

src/goto-instrument/contracts/contracts.cpp

@@ -1311,12 +1311,14 @@ void code_contractst::enforce_contract(const irep_idt &function)
   goto_functions.function_map.erase(old_function);
 
   // Place a new symbol with the mangled name into the symbol table
-  symbolt mangled_sym;
+  source_locationt sl;
+  sl.set_file("instrumented for code contracts");
+  sl.set_line("0");
   const symbolt *original_sym = symbol_table.lookup(original);
-  mangled_sym = *original_sym;
+  symbolt mangled_sym = *original_sym;
   mangled_sym.name = mangled;
   mangled_sym.base_name = mangled;
-  mangled_sym.location = original_sym->location;
+  mangled_sym.location = sl;
   const auto mangled_found = symbol_table.insert(std::move(mangled_sym));
   INVARIANT(
     mangled_found.second,

src/goto-instrument/function.cpp

@@ -34,21 +34,25 @@ code_function_callt function_to_call(
 
   if(s_it==symbol_table.symbols.end())
   {
+    // This has to be dead code: a symbol table must contain all functions that
+    // appear in goto_functions.
+    UNREACHABLE;
+#if 0
+
     // not there
     auto p = pointer_type(char_type());
     p.base_type().set(ID_C_constant, true);
 
     const code_typet function_type({code_typet::parametert(p)}, empty_typet());
 
-    symbolt new_symbol;
-    new_symbol.name=id;
+    symbolt new_symbol{id, function_type, irep_idt{}};
     new_symbol.base_name=id;
-    new_symbol.type=function_type;
 
     symbol_table.insert(std::move(new_symbol));
 
     s_it=symbol_table.symbols.find(id);
     assert(s_it!=symbol_table.symbols.end());
+#endif
   }
 
   // signature is expected to be

src/goto-instrument/goto_program2code.cpp

@@ -1867,10 +1867,8 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
           base_name="nondet_"+std::to_string(count);
         }
 
-        symbolt symbol;
+        symbolt symbol{base_name, code_typet({}, expr.type()), ID_C};
         symbol.base_name=base_name;
-        symbol.name=base_name;
-        symbol.type = code_typet({}, expr.type());
         id=symbol.name;
 
         symbol_table.insert(std::move(symbol));

src/goto-instrument/race_check.cpp

@@ -75,10 +75,9 @@ const symbolt &w_guardst::get_guard_symbol(const irep_idt &object)
 
   w_guards.push_back(identifier);
 
-  symbolt new_symbol;
-  new_symbol.name=identifier;
+  symbolt new_symbol{
+    identifier, bool_typet(), symbol_table.lookup_ref(object).mode};
   new_symbol.base_name=identifier;
-  new_symbol.type=bool_typet();
   new_symbol.is_static_lifetime=true;
   new_symbol.value=false_exprt();
 

src/goto-instrument/stack_depth.cpp

@@ -28,14 +28,11 @@ static symbol_exprt add_stack_depth_symbol(
   const irep_idt identifier="$stack_depth";
   unsignedbv_typet type(sizeof(std::size_t)*8);
 
-  symbolt new_symbol;
-  new_symbol.name=identifier;
+  symbolt new_symbol{identifier, type, ID_C};
   new_symbol.base_name=identifier;
   new_symbol.pretty_name=identifier;
-  new_symbol.type=type;
   new_symbol.is_static_lifetime=true;
   new_symbol.value=from_integer(0, type);
-  new_symbol.mode=ID_C;
   new_symbol.is_thread_local=true;
   new_symbol.is_lvalue=true;
 

src/goto-instrument/uninitialized.cpp

@@ -84,15 +84,12 @@ void uninitializedt::add_assertions(
   {
     const symbolt &symbol=ns.lookup(*it);
 
-    symbolt new_symbol;
-    new_symbol.name=id2string(symbol.name)+"#initialized";
-    new_symbol.type=bool_typet();
+    symbolt new_symbol{
+      id2string(symbol.name) + "#initialized", bool_typet(), symbol.mode};
     new_symbol.base_name=id2string(symbol.base_name)+"#initialized";
     new_symbol.location=symbol.location;
-    new_symbol.mode=symbol.mode;
     new_symbol.module=symbol.module;
     new_symbol.is_thread_local=true;
-    new_symbol.is_static_lifetime=false;
     new_symbol.is_file_local=true;
     new_symbol.is_lvalue=true;