Use constructors to construct objects

This is some drive-by cleanup resulting from reviewing #3067. Instead of
incrementally constructing objects do RAII.

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -288,7 +288,7 @@ static void instrument_start_thread(
 
   // Create global variable __CPROVER__next_thread_id. Used as a counter
   // in-order to to assign ids to new threads.
-  const symbolt &next_symbol =
+  const symbol_exprt next_symbol_expr =
     add_or_get_symbol(
         symbol_table, next_thread_id, next_thread_id,
         java_int_type(),
@@ -320,14 +320,11 @@ static void instrument_start_thread(
   codet tmp_a(ID_start_thread);
   tmp_a.set(ID_destination, lbl1);
   code_gotot tmp_b(lbl2);
-  code_labelt tmp_c(lbl1);
-  tmp_c.op0() = codet(ID_skip);
+  const code_labelt tmp_c(lbl1, codet(ID_skip));
 
-  exprt plus(ID_plus, java_int_type());
-  plus.copy_to_operands(next_symbol.symbol_expr());
-  plus.copy_to_operands(from_integer(1, java_int_type()));
-  code_assignt tmp_d(next_symbol.symbol_expr(), plus);
-  code_assignt tmp_e(current_symbol.symbol_expr(), next_symbol.symbol_expr());
+  const plus_exprt plus(next_symbol_expr, from_integer(1, java_int_type()));
+  const code_assignt tmp_d(next_symbol_expr, plus);
+  const code_assignt tmp_e(current_symbol.symbol_expr(), next_symbol_expr);
 
   code_blockt block;
   block.add(tmp_a);
@@ -368,8 +365,7 @@ static void instrument_end_thread(
   // A: codet(id=ID_end_thread)
   // B: codet(id=ID_label,label= __CPROVER_THREAD_EXIT_<ID>)
   codet tmp_a(ID_end_thread);
-  code_labelt tmp_b(lbl2);
-  tmp_b.op0() = codet(ID_skip);
+  const code_labelt tmp_b(lbl2, codet(ID_skip));
 
   code_blockt block;
   block.add(tmp_a);

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1742,7 +1742,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
           for(auto &expr : stack)
           {
             assert(has_prefix(os_it->get_string(ID_C_base_name), "$stack"));
-            symbol_exprt lhs=to_symbol_expr(*os_it);
+            const symbol_exprt &lhs = to_symbol_expr(*os_it);
             code_assignt a(lhs, expr);
             more_code.copy_to_operands(a);
 
@@ -2737,13 +2737,11 @@ codet java_bytecode_convert_methodt::convert_iinc(
     bytecode_write_typet::VARIABLE,
     to_symbol_expr(locvar).get_identifier());
 
-  code_assignt code_assign;
-  code_assign.lhs() = variable(arg0, 'i', address, NO_CAST);
-  exprt arg1_int_type = arg1;
-  if(arg1.type() != java_int_type())
-    arg1_int_type.make_typecast(java_int_type());
-  code_assign.rhs() =
-    plus_exprt(variable(arg0, 'i', address, CAST_AS_NEEDED), arg1_int_type);
+  const exprt arg1_int_type =
+    typecast_exprt::conditional_cast(arg1, java_int_type());
+  const code_assignt code_assign(
+    variable(arg0, 'i', address, NO_CAST),
+    plus_exprt(variable(arg0, 'i', address, CAST_AS_NEEDED), arg1_int_type));
   block.copy_to_operands(code_assign);
   return block;
 }

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -169,8 +169,8 @@ static void java_static_lifetime_init(
         // Argument order is: name, isAnnotation, isArray, isInterface,
         // isSynthetic, isLocalClass, isMemberClass, isEnum
 
-        code_function_callt initializer_call;
-        initializer_call.function() = class_literal_init_method->symbol_expr();
+        code_function_callt initializer_call(
+          class_literal_init_method->symbol_expr());
 
         code_function_callt::argumentst &args = initializer_call.arguments();
 
@@ -676,10 +676,8 @@ bool generate_java_start_function(
       return true; // give up with error
     }
 
-    code_function_callt call_init;
-    call_init.lhs().make_nil();
+    code_function_callt call_init(init_it->second.symbol_expr());
     call_init.add_source_location()=symbol.location;
-    call_init.function()=init_it->second.symbol_expr();
 
     init_code.move_to_operands(call_init);
   }
@@ -689,15 +687,13 @@ bool generate_java_start_function(
   // where return is a new variable
   // and arg1 ... argn are constructed below as well
 
-  code_function_callt call_main;
-
   source_locationt loc=symbol.location;
   loc.set_function(symbol.name);
   source_locationt &dloc=loc;
 
   // function to call
+  code_function_callt call_main(symbol.symbol_expr());
   call_main.add_source_location()=dloc;
-  call_main.function()=symbol.symbol_expr();
   call_main.function().add_source_location()=dloc;
 
   // if the method return type is not void, store return value in a new variable

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -213,7 +213,7 @@ exprt allocate_dynamic_object(
       ID_java,
       symbol_table);
     symbols_created.push_back(&malloc_sym);
-    code_assignt assign=code_assignt(malloc_sym.symbol_expr(), malloc_expr);
+    code_assignt assign(malloc_sym.symbol_expr(), malloc_expr);
     assign.add_source_location()=loc;
     output_code.copy_to_operands(assign);
     exprt malloc_symbol_expr=malloc_sym.symbol_expr();
@@ -1391,7 +1391,7 @@ void java_object_factoryt::gen_nondet_array_init(
     symbol_table);
   symbols_created.push_back(&array_init_symbol);
   const auto &array_init_symexpr=array_init_symbol.symbol_expr();
-  codet data_assign=code_assignt(array_init_symexpr, init_array_expr);
+  code_assignt data_assign(array_init_symexpr, init_array_expr);
   data_assign.add_source_location()=loc;
   assignments.copy_to_operands(data_assign);
 

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -208,17 +208,15 @@ static void clinit_wrapper_do_recursive_calls(
     auto findit = symbol_table.symbols.find(base_init_routine);
     if(findit == symbol_table.symbols.end())
       continue;
-    code_function_callt call_base;
-    call_base.function() = findit->second.symbol_expr();
+    const code_function_callt call_base(findit->second.symbol_expr());
     init_body.move_to_operands(call_base);
   }
 
   const irep_idt &real_clinit_name = clinit_function_name(class_name);
   auto find_sym_it = symbol_table.symbols.find(real_clinit_name);
   if(find_sym_it != symbol_table.symbols.end())
   {
-    code_function_callt call_real_init;
-    call_real_init.function() = find_sym_it->second.symbol_expr();
+    const code_function_callt call_real_init(find_sym_it->second.symbol_expr());
     init_body.move_to_operands(call_real_init);
   }