Replace all uses of deprecated symbol_exprt constructors

This helps type safety has it avoids constructing symbol_exprts that never get
a proper type (or identifier).

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1536,13 +1536,12 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="getstatic")
     {
       PRECONDITION(op.empty() && results.size() == 1);
-      symbol_exprt symbol_expr(arg0.type());
       const auto &field_name=arg0.get_string(ID_component_name);
       const bool is_assertions_disabled_field=
         field_name.find("$assertionsDisabled")!=std::string::npos;
 
-      symbol_expr.set_identifier(
-        get_static_field(arg0.get_string(ID_class), field_name));
+      const symbol_exprt symbol_expr(
+        get_static_field(arg0.get_string(ID_class), field_name), arg0.type());
 
       INVARIANT(
         symbol_table.has_symbol(symbol_expr.get_identifier()),
@@ -1559,10 +1558,10 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="putstatic")
     {
       PRECONDITION(op.size() == 1 && results.empty());
-      symbol_exprt symbol_expr(arg0.type());
       const auto &field_name=arg0.get_string(ID_component_name);
-      symbol_expr.set_identifier(
-        get_static_field(arg0.get_string(ID_class), field_name));
+
+      const symbol_exprt symbol_expr(
+        get_static_field(arg0.get_string(ID_class), field_name), arg0.type());
 
       INVARIANT(
         symbol_table.has_symbol(symbol_expr.get_identifier()),

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -119,7 +119,11 @@ class java_bytecode_convert_methodt:public messaget
     bool is_parameter;
     std::vector<holet> holes;
 
-    variablet() : symbol_expr(), start_pc(0), length(0), is_parameter(false)
+    variablet()
+      : symbol_expr("", typet()),
+        start_pc(0),
+        length(0),
+        is_parameter(false)
     {
     }
   };

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -1600,7 +1600,7 @@ exprt java_bytecode_parsert::get_relement_value()
   case 'c':
     {
       u2 class_info_index = read_u2();
-      return symbol_exprt(pool_entry(class_info_index).s);
+      return symbol_exprt(pool_entry(class_info_index).s, typet());
     }
 
   case '@':

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -1558,14 +1558,14 @@ code_blockt java_string_library_preprocesst::make_object_get_class_code(
     loc);
 
   // > class1 = Class.forName(string1)
+  java_method_typet fun_type(
+    {java_method_typet::parametert(string_ptr_type)}, class_type);
   code_function_callt fun_call(
     class1,
     symbol_exprt(
-      "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;"),
+      "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;",
+      std::move(fun_type)),
     {string1});
-  const java_method_typet fun_type(
-    {java_method_typet::parametert(string_ptr_type)}, class_type);
-  fun_call.function().type()=fun_type;
   code.add(fun_call, loc);
 
   // > return class1;

jbmc/src/java_bytecode/java_utils.cpp

@@ -285,7 +285,8 @@ exprt make_function_application(
   declare_function(fun_name, type, symbol_table);
 
   // Function application
-  return function_application_exprt(symbol_exprt(fun_name), arguments, type);
+  return function_application_exprt(
+    symbol_exprt(fun_name, typet()), arguments, type);
 }
 
 /// Strip java:: prefix from given identifier

jbmc/src/java_bytecode/simple_method_stubbing.cpp

@@ -170,7 +170,8 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
       symbol_table);
     const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr();
     code_assignt get_argument(
-      init_symbol_expression, symbol_exprt(this_argument.get_identifier()));
+      init_symbol_expression,
+      symbol_exprt(this_argument.get_identifier(), this_argument.type()));
     get_argument.add_source_location() = synthesized_source_location;
     new_instructions.add(get_argument);
     create_method_stub_at(

jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -185,7 +185,7 @@ SCENARIO("instantiate_not_contains",
   {
     // Creating "ab".lastIndexOf("b", 0)
     const function_application_exprt func(
-      symbol_exprt(ID_cprover_string_last_index_of_func),
+      symbol_exprt(ID_cprover_string_last_index_of_func, typet()),
       {ab, b, from_integer(2)},
       t.length_type());
 
@@ -215,7 +215,7 @@ SCENARIO("instantiate_not_contains",
         simplify(sc.premise, empty_ns);
         simplify(sc.s0, empty_ns);
         simplify(sc.s1, empty_ns);
-        witnesses[sc] = generator.fresh_symbol("w", t.witness_type());
+        witnesses.emplace(sc, generator.fresh_symbol("w", t.witness_type()));
         nc_axioms.push_back(sc);
         return accu + to_string(sc) + "\n\n";
       });
@@ -287,7 +287,7 @@ SCENARIO("instantiate_not_contains",
     // Create witness for axiom
     string_constraint_generatort generator(empty_ns);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
-    witnesses[vacuous] = generator.fresh_symbol("w", t.witness_type());
+    witnesses.emplace(vacuous, generator.fresh_symbol("w", t.witness_type()));
 
     INFO("Original axiom:\n");
     INFO(to_string(vacuous) + "\n\n");
@@ -337,7 +337,7 @@ SCENARIO("instantiate_not_contains",
     // Create witness for axiom
     string_constraint_generatort generator(empty_ns);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
-    witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
+    witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
 
     INFO("Original axiom:\n");
     INFO(to_string(trivial) + "\n\n");
@@ -388,7 +388,7 @@ SCENARIO("instantiate_not_contains",
     // Create witness for axiom
     string_constraint_generatort generator(empty_ns);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
-    witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
+    witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
 
     INFO("Original axiom:\n");
     INFO(to_string(trivial) + "\n\n");
@@ -441,7 +441,7 @@ SCENARIO("instantiate_not_contains",
     // Create witness for axiom
     string_constraint_generatort generator(empty_ns);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
-    witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
+    witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
 
     INFO("Original axiom:\n");
     INFO(to_string(trivial) + "\n\n");
@@ -492,7 +492,7 @@ SCENARIO("instantiate_not_contains",
     // Create witness for axiom
     string_constraint_generatort generator(empty_ns);
     std::unordered_map<string_not_contains_constraintt, symbol_exprt> witnesses;
-    witnesses[trivial] = generator.fresh_symbol("w", t.witness_type());
+    witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type()));
 
     INFO("Original axiom:\n");
     INFO(to_string(trivial) + "\n\n");

jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp

@@ -68,19 +68,19 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
 
     // fun1 is s3 = s1.concat(s2)
     const function_application_exprt fun1(
-      symbol_exprt(ID_cprover_string_concat_func),
+      symbol_exprt(ID_cprover_string_concat_func, typet()),
       {string3.op0(), string3.op1(), string1, string2},
       fun_type);
 
     // fun2 is s5 = s3.concat(s4)
     const function_application_exprt fun2(
-      symbol_exprt(ID_cprover_string_concat_func),
+      symbol_exprt(ID_cprover_string_concat_func, typet()),
       {string5.op0(), string5.op1(), string3, string4},
       fun_type);
 
     // fun3 is s6 = s5.concat(s2)
     const function_application_exprt fun3(
-      symbol_exprt(ID_cprover_string_concat_func),
+      symbol_exprt(ID_cprover_string_concat_func, typet()),
       {string6.op0(), string6.op1(), string5, string2},
       fun_type);
 

src/analyses/constant_propagator.cpp

@@ -649,7 +649,8 @@ bool constant_propagator_domaint::partial_evaluate(
   // if the current rounding mode is top we can
   // still get a non-top result by trying all rounding
   // modes and checking if the results are all the same
-  if(!known_values.is_constant(symbol_exprt(ID_cprover_rounding_mode_str)))
+  if(!known_values.is_constant(
+       symbol_exprt(ID_cprover_rounding_mode_str, typet())))
   {
     return partial_evaluate_with_all_rounding_modes(known_values, expr, ns);
   }

src/analyses/locals.cpp

@@ -21,12 +21,13 @@ void localst::build(const goto_functiont &goto_function)
     if(it->is_decl())
     {
       const code_declt &code_decl=to_code_decl(it->code);
-      locals_map[code_decl.get_identifier()] = code_decl.symbol();
+      locals_map.emplace(code_decl.get_identifier(), code_decl.symbol());
     }
 
   for(const auto &param : goto_function.type.parameters())
-    locals_map[param.get_identifier()]=
-      symbol_exprt(param.get_identifier(), param.type());
+    locals_map.emplace(
+      param.get_identifier(),
+      symbol_exprt(param.get_identifier(), param.type()));
 }
 
 void localst::output(std::ostream &out) const