Use code_ifthenelset constructor

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

@@ -251,10 +251,9 @@ code_ifthenelset java_bytecode_instrumentt::check_class_cast(
     check_code=std::move(assert_class);
   }
 
-  code_ifthenelset conditional_check;
-  notequal_exprt op_not_null(null_check_op, null_pointer_exprt(voidptr));
-  conditional_check.cond()=std::move(op_not_null);
-  conditional_check.then_case()=std::move(check_code);
+  const code_ifthenelset conditional_check(
+    notequal_exprt(std::move(null_check_op), null_pointer_exprt(voidptr)),
+    std::move(check_code));
   return conditional_check;
 }
 

jbmc/src/java_bytecode/remove_instanceof.cpp

@@ -134,13 +134,6 @@ bool remove_instanceoft::lower_instanceof(
   // possible values of T.
   // (http://docs.oracle.com/javase/specs/jls/se7/html/jls-15.html#jls-15.20.2)
 
-  code_ifthenelset is_null_branch;
-  is_null_branch.cond() =
-    equal_exprt(
-      check_ptr, null_pointer_exprt(to_pointer_type(check_ptr.type())));
-  is_null_branch.then_case() =
-    code_assignt(instanceof_result_sym.symbol_expr(), false_exprt());
-
   code_blockt else_block;
   else_block.add(code_declt(clsid_tmp_sym.symbol_expr()));
   else_block.add(code_assignt(clsid_tmp_sym.symbol_expr(), object_clsid));
@@ -155,7 +148,11 @@ bool remove_instanceoft::lower_instanceof(
   else_block.add(
     code_assignt(instanceof_result_sym.symbol_expr(), disjunction(or_ops)));
 
-  is_null_branch.else_case() = std::move(else_block);
+  const code_ifthenelset is_null_branch(
+    equal_exprt(
+      check_ptr, null_pointer_exprt(to_pointer_type(check_ptr.type()))),
+    code_assignt(instanceof_result_sym.symbol_expr(), false_exprt()),
+    std::move(else_block));
 
   // Replace the instanceof construct with instanceof_result:
   expr = instanceof_result_sym.symbol_expr();

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -174,10 +174,10 @@ void symbol_factoryt::gen_nondet_init(
       auto set_null_inst=code_assignt(expr, null_pointer_exprt(pointer_type));
       set_null_inst.add_source_location()=loc;
 
-      code_ifthenelset null_check;
-      null_check.cond() = side_effect_expr_nondett(bool_typet(), loc);
-      null_check.then_case()=set_null_inst;
-      null_check.else_case()=non_null_inst;
+      code_ifthenelset null_check(
+        side_effect_expr_nondett(bool_typet(), loc),
+        std::move(set_null_inst),
+        std::move(non_null_inst));
 
       assignments.add(std::move(null_check));
     }