Use non-deprecated constructors for code*t

The default constructor for codet is deprecated.

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1206,7 +1206,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
       }
     }
 
-    codet catch_instruction;
+    codet catch_instruction(ID_nil);
 
     if(catch_type!=typet())
     {
@@ -1223,8 +1223,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
           "caught_exception",
           java_reference_type(catch_type));
       stack.push_back(catch_var);
-      code_landingpadt catch_statement(catch_var);
-      catch_instruction=catch_statement;
+      catch_instruction = code_landingpadt(catch_var);
     }
 
     exprt::operandst op = pop(stmt_bytecode_info.pop);
@@ -1677,7 +1676,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     // Finally if this is the beginning of a catch block (already determined
     // before the big bytecode switch), insert the exception 'landing pad'
     // instruction before the actual instruction:
-    if(catch_instruction!=codet())
+    if(catch_instruction.get_statement() != ID_nil)
     {
       c.make_block();
       c.operands().insert(c.operands().begin(), catch_instruction);
@@ -1930,9 +1929,6 @@ code_switcht java_bytecode_convert_methodt::convert_switch(
   const source_locationt &location)
 {
   // we turn into switch-case
-  code_switcht code_switch;
-  code_switch.add_source_location() = location;
-  code_switch.value() = op[0];
   code_blockt code_block;
   code_block.add_source_location() = location;
 
@@ -1942,36 +1938,40 @@ code_switcht java_bytecode_convert_methodt::convert_switch(
   {
     if(is_label)
     {
-      code_switch_caset code_case;
-      code_case.add_source_location() = location;
-
       const mp_integer number = numeric_cast_v<mp_integer>(*a_it);
       // The switch case does not contain any code, it just branches via a GOTO
       // to the jump target of the tableswitch/lookupswitch case at
       // hand. Therefore we consider this code to belong to the source bytecode
       // instruction and not the target instruction.
       const method_offsett label_number =
         numeric_cast_v<method_offsett>(number);
-      code_case.code() = code_gotot(label(std::to_string(label_number)));
-      code_case.code().add_source_location() = location;
+      code_gotot code(label(std::to_string(label_number)));
+      code.add_source_location() = location;
 
       if(a_it == args.begin())
+      {
+        code_switch_caset code_case(nil_exprt(), std::move(code));
+        code_case.add_source_location() = location;
         code_case.set_default();
+
+        code_block.add(std::move(code_case));
+      }
       else
       {
-        auto prev = a_it;
-        prev--;
-        code_case.case_op() = *prev;
-        if(code_case.case_op().type() != op[0].type())
-          code_case.case_op().make_typecast(op[0].type());
-        code_case.case_op().add_source_location() = location;
-      }
+        exprt case_op =
+          typecast_exprt::conditional_cast(*std::prev(a_it), op[0].type());
+        case_op.add_source_location() = location;
+
+        code_switch_caset code_case(std::move(case_op), std::move(code));
+        code_case.add_source_location() = location;
 
-      code_block.add(code_case);
+        code_block.add(std::move(code_case));
+      }
     }
   }
 
-  code_switch.body() = code_block;
+  code_switcht code_switch(op[0], code_block);
+  code_switch.add_source_location() = location;
   return code_switch;
 }
 
@@ -2150,25 +2150,22 @@ void java_bytecode_convert_methodt::convert_invoke(
     }
   }
 
-  code_function_callt call;
   location.set_function(method_id);
 
-  call.add_source_location() = location;
-  call.arguments() = pop(parameters.size());
+  code_function_callt::argumentst arguments = pop(parameters.size());
 
   // double-check a bit
-  if(use_this)
-  {
-    const exprt &this_arg = call.arguments().front();
-    INVARIANT(
-      this_arg.type().id() == ID_pointer, "first argument must be a pointer");
-  }
+  INVARIANT(
+    !use_this || arguments.front().type().id() == ID_pointer,
+    "first argument must be a pointer");
 
   // do some type adjustment for the arguments,
   // as Java promotes arguments
   // Also cast pointers since intermediate locals
   // can be void*.
-
+  INVARIANT(
+    parameters.size() <= arguments.size(),
+    "for each parameter there must be an argument");
   for(std::size_t i = 0; i < parameters.size(); i++)
   {
     const typet &type = parameters[i].type();
@@ -2177,21 +2174,20 @@ void java_bytecode_convert_methodt::convert_invoke(
       type == java_byte_type() || type == java_short_type() ||
       type.id() == ID_pointer)
     {
-      assert(i < call.arguments().size());
-      if(type != call.arguments()[i].type())
-        call.arguments()[i].make_typecast(type);
+      if(type != arguments[i].type())
+        arguments[i].make_typecast(type);
     }
   }
 
   // do some type adjustment for return values
-
+  exprt lhs = nil_exprt();
   const typet &return_type = method_type.return_type();
 
   if(return_type.id() != ID_empty)
   {
     // return types are promoted in Java
-    call.lhs() = tmp_variable("return", return_type);
-    exprt promoted = java_bytecode_promotion(call.lhs());
+    lhs = tmp_variable("return", return_type);
+    exprt promoted = java_bytecode_promotion(lhs);
     results.resize(1);
     results[0] = promoted;
   }
@@ -2233,19 +2229,20 @@ void java_bytecode_convert_methodt::convert_invoke(
     symbol_table.add(symbol);
   }
 
+  exprt function;
   if(is_virtual)
   {
     // dynamic binding
-    assert(use_this);
-    assert(!call.arguments().empty());
-    call.function() = arg0;
+    PRECONDITION(use_this);
+    PRECONDITION(!arguments.empty());
+    function = arg0;
     // Populate needed methods later,
     // once we know what object types can exist.
   }
   else
   {
     // static binding
-    call.function() = symbol_exprt(invoked_method_id, method_type);
+    function = symbol_exprt(invoked_method_id, method_type);
     if(needed_lazy_methods)
     {
       needed_lazy_methods->add_needed_method(invoked_method_id);
@@ -2254,6 +2251,9 @@ void java_bytecode_convert_methodt::convert_invoke(
     }
   }
 
+  code_function_callt call(
+    std::move(lhs), std::move(function), std::move(arguments));
+  call.add_source_location() = location;
   call.function().add_source_location() = location;
 
   // Replacing call if it is a function of the Character library,
@@ -2313,16 +2313,14 @@ void java_bytecode_convert_methodt::convert_athrow(
     // we translate athrow into
     // ASSERT false;
     // ASSUME false:
-    code_assertt assert_code;
-    assert_code.assertion() = false_exprt();
+    code_assertt assert_code(false_exprt{});
     source_locationt assert_location = location; // copy
     assert_location.set_comment("assertion at " + location.as_string());
     assert_location.set("user-provided", true);
     assert_location.set_property_class(ID_assertion);
     assert_code.add_source_location() = assert_location;
 
-    code_assumet assume_code;
-    assume_code.assumption() = false_exprt();
+    code_assumet assume_code(false_exprt{});
     source_locationt assume_location = location; // copy
     assume_location.set("user-provided", true);
     assume_code.add_source_location() = assume_location;

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

@@ -225,18 +225,17 @@ code_ifthenelset java_bytecode_instrumentt::check_class_cast(
     class1, ID_java_instanceof, class2);
 
   pointer_typet voidptr=pointer_type(empty_typet());
-  exprt null_check_op=class1;
-  if(null_check_op.type()!=voidptr)
-    null_check_op.make_typecast(voidptr);
+  exprt null_check_op = typecast_exprt::conditional_cast(class1, voidptr);
 
-  codet check_code;
   if(throw_runtime_exceptions)
   {
-    check_code=
+    return code_ifthenelset(
+      notequal_exprt(
+        std::move(null_check_op), null_pointer_exprt(std::move(voidptr))),
       throw_exception(
         not_exprt(class_cast_check),
         original_loc,
-        "java.lang.ClassCastException");
+        "java.lang.ClassCastException"));
   }
   else
   {
@@ -246,12 +245,11 @@ code_ifthenelset java_bytecode_instrumentt::check_class_cast(
 
     codet assert_class = create_fatal_assertion(class_cast_check, check_loc);
 
-    check_code=std::move(assert_class);
+    return code_ifthenelset(
+      notequal_exprt(
+        std::move(null_check_op), null_pointer_exprt(std::move(voidptr))),
+      std::move(assert_class));
   }
-
-  return code_ifthenelset(
-    notequal_exprt(std::move(null_check_op), null_pointer_exprt(voidptr)),
-    std::move(check_code));
 }
 
 /// Checks whether \p expr is null and throws NullPointerException/

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -358,7 +358,6 @@ exprt::operandst java_build_arguments(
       INVARIANT(!is_this, "We cannot have different types for `this` here");
       // create a non-deterministic switch between all possible values for the
       // type of the parameter.
-      code_switcht code_switch;
 
       // the idea is to get a new symbol for the parameter value `tmp`
 
@@ -385,8 +384,10 @@ exprt::operandst java_build_arguments(
         symbol_table);
       main_arguments[param_number] = result_symbol.symbol_expr();
 
-      std::vector<codet> cases(alternatives.size());
-      const auto initialize_parameter = [&](const struct_tag_typet &type) {
+      std::vector<codet> cases;
+      cases.reserve(alternatives.size());
+      for(const auto &type : alternatives)
+      {
         code_blockt init_code_for_type;
         exprt init_expr_for_parameter = object_factory(
           java_reference_type(type),
@@ -402,14 +403,8 @@ exprt::operandst java_build_arguments(
           code_assignt(
             result_symbol.symbol_expr(),
             typecast_exprt(init_expr_for_parameter, p.type())));
-        return init_code_for_type;
-      };
-
-      std::transform(
-        alternatives.begin(),
-        alternatives.end(),
-        cases.begin(),
-        initialize_parameter);
+        cases.push_back(init_code_for_type);
+      }
 
       init_code.add(
         generate_nondet_switch(

src/ansi-c/c_typecheck_base.cpp

@@ -648,7 +648,7 @@ void c_typecheck_baset::typecheck_declaration(
     // mark as 'already typechecked'
     make_already_typechecked(declaration.type());
 
-    codet contract;
+    codet contract(ID_nil);
 
     {
       exprt spec_requires=

src/cpp/cpp_constructor.cpp

@@ -144,8 +144,7 @@ optionalt<codet> cpp_typecheckt::cpp_constructor(
       side_effect_expr_assignt assign(
         object_tc, operands_tc.front(), typet(), source_location);
       typecheck_side_effect_assignment(assign);
-      code_expressiont new_code;
-      new_code.expression()=assign;
+      code_expressiont new_code(assign);
       return std::move(new_code);
     }
     else
@@ -225,9 +224,9 @@ optionalt<codet> cpp_typecheckt::cpp_constructor(
 
     side_effect_expr_function_callt function_call(
       cpp_namet(constructor_name, source_location).as_expr(),
-      operands_tc);
-
-    function_call.add_source_location()=source_location;
+      operands_tc,
+      typet(),
+      source_location);
 
     typecheck_side_effect_function_call(function_call);
     assert(function_call.get(ID_statement)==ID_temporary_object);

src/cpp/cpp_destructor.cpp

@@ -20,9 +20,6 @@ optionalt<codet> cpp_typecheckt::cpp_destructor(
   const source_locationt &source_location,
   const exprt &object)
 {
-  codet new_code;
-  new_code.add_source_location()=source_location;
-
   elaborate_class_template(object.type());
 
   typet tmp_type(follow(object.type()));
@@ -53,9 +50,8 @@ optionalt<codet> cpp_typecheckt::cpp_destructor(
       throw 0;
     }
 
-    new_code.type().id(ID_code);
+    code_blockt new_code;
     new_code.add_source_location()=source_location;
-    new_code.set_statement(ID_block);
 
     // for each element of the array, call the destructor
     for(mp_integer i=0; i < s; ++i)
@@ -70,6 +66,8 @@ optionalt<codet> cpp_typecheckt::cpp_destructor(
       if(i_code.has_value())
         new_code.add_to_operands(std::move(i_code.value()));
     }
+
+    return std::move(new_code);
   }
   else
   {
@@ -108,16 +106,15 @@ optionalt<codet> cpp_typecheckt::cpp_destructor(
     member.add(ID_component_cpp_name) = cpp_name;
     member.copy_to_operands(object);
 
-    side_effect_expr_function_callt function_call;
-    function_call.add_source_location()=source_location;
-    function_call.function().swap(member);
+    side_effect_expr_function_callt function_call(
+      std::move(member), {}, typet{}, source_location);
 
     typecheck_side_effect_function_call(function_call);
     already_typechecked(function_call);
 
-    new_code = code_expressiont(function_call);
+    code_expressiont new_code(function_call);
     new_code.add_source_location() = source_location;
-  }
 
-  return new_code;
+    return std::move(new_code);
+  }
 }

src/cpp/cpp_typecheck.h

@@ -124,9 +124,7 @@ class cpp_typecheckt:public c_typecheck_baset
 
   void convert_pmop(exprt &expr);
 
-  void convert_anonymous_union(
-    cpp_declarationt &declaration,
-    codet &new_code);
+  codet convert_anonymous_union(cpp_declarationt &declaration);
 
   void convert_anon_struct_union_member(
     const cpp_declarationt &declaration,