Merge pull request #3932 from tautschnig/deprecation-switch

Avoid default code_switch(_case)t's default constructor [blocks: #3800]

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1929,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;
 
@@ -1941,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], std::move(code_block));
+  code_switch.add_source_location() = location;
   return code_switch;
 }
 

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/goto-instrument/goto_program2code.cpp

@@ -894,9 +894,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch(
     return convert_goto_if(target, upper_bound, dest);
 
   // maybe, let's try some more
-  code_switcht s;
-  s.value()=to_equal_expr(eq_cand).lhs();
-  s.body()=code_blockt();
+  code_switcht s(to_equal_expr(eq_cand).lhs(), code_blockt());
 
   copy_source_location(target, s);
 
@@ -962,7 +960,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch(
       it!=cases.end();
       ++it)
   {
-    code_switch_caset csc;
+    code_switch_caset csc(nil_exprt{}, code_blockt{});
     // branch condition is nil_exprt for default case;
     if(it->value.is_nil())
       csc.set_default();