diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 40d8ad6e7c5..1b56a221e4f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -2166,8 +2166,7 @@ void java_bytecode_convert_methodt::convert_invoke( type == java_byte_type() || type == java_short_type() || type.id() == ID_pointer) { - if(type != arguments[i].type()) - arguments[i].make_typecast(type); + arguments[i] = typecast_exprt::conditional_cast(arguments[i], type); } } diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp index 117294b423e..3b11e293fdf 100644 --- a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp @@ -225,9 +225,7 @@ code_ifthenelset java_bytecode_instrumentt::check_class_cast( class1, ID_java_instanceof, class2); pointer_typet voidptr = pointer_type(java_void_type()); - 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); optionalt check_code; if(throw_runtime_exceptions) diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index fbef18a84e7..231d21a4fd9 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -406,10 +406,10 @@ bool generate_ansi_c_start_function( zero_string.type().subtype()=char_type(); zero_string.type().set(ID_size, "infinity"); const index_exprt index(zero_string, from_integer(0, uint_type())); - exprt address_of=address_of_exprt(index, pointer_type(char_type())); - - if(argv_symbol.type.subtype()!=address_of.type()) - address_of.make_typecast(argv_symbol.type.subtype()); + exprt address_of = + typecast_exprt::conditional_cast( + address_of_exprt(index, pointer_type(char_type())), + argv_symbol.type.subtype()); // assign argv[*] to the address of a string-object array_of_exprt array_of(address_of, argv_symbol.type); diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 5d3ca4a2015..612fb306d6b 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2596,10 +2596,11 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - expr.arguments()[0].make_typecast(bool_typet()); - make_constant(expr.arguments()[0]); + exprt arg0 = + typecast_exprt::conditional_cast(expr.arguments()[0], bool_typet()); + make_constant(arg0); - if(expr.arguments()[0].is_true()) + if(arg0.is_true()) return expr.arguments()[1]; else return expr.arguments()[2]; @@ -2953,7 +2954,7 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr) is_number(o_type1)) { // convert op1 to the vector type - op1.make_typecast(o_type0); + op1 = typecast_exprt(op1, o_type0); expr.type() = o_type0; return; } @@ -2962,7 +2963,7 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr) is_number(o_type0)) { // convert op0 to the vector type - op0.make_typecast(o_type1); + op0 = typecast_exprt(op0, o_type1); expr.type() = o_type1; return; } diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp index 3e56a156132..358dec5c59f 100644 --- a/src/cpp/cpp_typecheck_conversions.cpp +++ b/src/cpp/cpp_typecheck_conversions.cpp @@ -210,8 +210,7 @@ bool cpp_typecheckt::standard_conversion_integral_promotion( std::size_t width=to_signedbv_type(expr.type()).get_width(); if(width >= config.ansi_c.int_width) return false; - new_expr=expr; - new_expr.make_typecast(int_type); + new_expr = typecast_exprt(expr, int_type); return true; } @@ -220,24 +219,19 @@ bool cpp_typecheckt::standard_conversion_integral_promotion( std::size_t width=to_unsignedbv_type(expr.type()).get_width(); if(width >= config.ansi_c.int_width) return false; - new_expr=expr; - if(width==config.ansi_c.int_width) - int_type.id(ID_unsignedbv); - new_expr.make_typecast(int_type); + new_expr = typecast_exprt(expr, int_type); return true; } if(expr.type().id() == ID_bool || expr.type().id() == ID_c_bool) { - new_expr = expr; - new_expr.make_typecast(int_type); + new_expr = typecast_exprt(expr, int_type); return true; } if(expr.type().id()==ID_c_enum_tag) { - new_expr=expr; - new_expr.make_typecast(int_type); + new_expr = typecast_exprt(expr, int_type); return true; } @@ -271,8 +265,7 @@ bool cpp_typecheckt::standard_conversion_floating_point_promotion( c_qualifierst qual_from; qual_from.read(expr.type()); - new_expr=expr; - new_expr.make_typecast(double_type()); + new_expr = typecast_exprt(expr, double_type()); qual_from.write(new_expr.type()); return true; @@ -328,8 +321,7 @@ bool cpp_typecheckt::standard_conversion_integral_conversion( c_qualifierst qual_from; qual_from.read(expr.type()); - new_expr=expr; - new_expr.make_typecast(type); + new_expr = typecast_exprt::conditional_cast(expr, type); qual_from.write(new_expr.type()); return true; @@ -382,8 +374,7 @@ bool cpp_typecheckt::standard_conversion_floating_integral_conversion( c_qualifierst qual_from; qual_from.read(expr.type()); - new_expr=expr; - new_expr.make_typecast(type); + new_expr = typecast_exprt::conditional_cast(expr, type); qual_from.write(new_expr.type()); return true; @@ -425,8 +416,7 @@ bool cpp_typecheckt::standard_conversion_floating_point_conversion( c_qualifierst qual_from; qual_from.read(expr.type()); - new_expr=expr; - new_expr.make_typecast(type); + new_expr = typecast_exprt::conditional_cast(expr, type); qual_from.write(new_expr.type()); return true; @@ -508,8 +498,7 @@ bool cpp_typecheckt::standard_conversion_pointer( { c_qualifierst qual_from; qual_from.read(expr.type().subtype()); - new_expr=expr; - new_expr.make_typecast(type); + new_expr = typecast_exprt::conditional_cast(expr, type); qual_from.write(new_expr.type().subtype()); return true; } @@ -614,8 +603,7 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member( if(expr.id()==ID_constant && expr.get(ID_value)==ID_NULL) { - new_expr=expr; - new_expr.make_typecast(type); + new_expr = typecast_exprt::conditional_cast(expr, type); return true; } @@ -627,8 +615,7 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member( if(subtype_typecast(to_struct, from_struct)) { - new_expr=expr; - new_expr.make_typecast(type); + new_expr = typecast_exprt::conditional_cast(expr, type); return true; } @@ -664,8 +651,7 @@ bool cpp_typecheckt::standard_conversion_boolean( typet Bool = c_bool_type(); qual_from.write(Bool); - new_expr=expr; - new_expr.make_typecast(Bool); + new_expr = typecast_exprt::conditional_cast(expr, Bool); return true; } @@ -705,7 +691,7 @@ bool cpp_typecheckt::standard_conversion_sequence( // we turn bit fields into their underlying type if(curr_expr.type().id()==ID_c_bit_field) - curr_expr.make_typecast(curr_expr.type().subtype()); + curr_expr = typecast_exprt(curr_expr, curr_expr.type().subtype()); if(curr_expr.type().id()==ID_array) { @@ -791,7 +777,7 @@ bool cpp_typecheckt::standard_conversion_sequence( if(expr.type().subtype().id()==ID_nullptr) { // std::nullptr_t to _any_ pointer type is ok - new_expr.make_typecast(type); + new_expr = typecast_exprt::conditional_cast(new_expr, type); } else if(!standard_conversion_pointer(curr_expr, type, new_expr)) { @@ -1278,7 +1264,7 @@ bool cpp_typecheckt::reference_binding( { c_qualifierst qual_from; qual_from.read(expr.type()); - new_expr.make_typecast(type); + new_expr = typecast_exprt::conditional_cast(new_expr, type); qual_from.write(new_expr.type().subtype()); } @@ -1805,8 +1791,7 @@ bool cpp_typecheckt::reinterpret_typecast( (type.id()==ID_unsignedbv || type.id()==ID_signedbv)) { // pointer to integer, always ok - new_expr=e; - new_expr.make_typecast(type); + new_expr = typecast_exprt::conditional_cast(e, type); return true; } @@ -1825,8 +1810,7 @@ bool cpp_typecheckt::reinterpret_typecast( } else { - new_expr=e; - new_expr.make_typecast(type); + new_expr = typecast_exprt::conditional_cast(e, type); } return true; } @@ -1837,16 +1821,13 @@ bool cpp_typecheckt::reinterpret_typecast( { // pointer to pointer: we ok it all. // This is more generous than the standard. - new_expr=expr; - new_expr.make_typecast(type); + new_expr = typecast_exprt::conditional_cast(expr, type); return true; } if(is_reference(type) && e.get_bool(ID_C_lvalue)) { - exprt tmp=address_of_exprt(e); - tmp.make_typecast(type); - new_expr.swap(tmp); + new_expr = typecast_exprt::conditional_cast(address_of_exprt(e), type); return true; } @@ -1919,8 +1900,7 @@ bool cpp_typecheckt::static_typecast( if(type.id()==ID_empty) { - new_expr=e; - new_expr.make_typecast(type); + new_expr = typecast_exprt::conditional_cast(e, type); return true; } @@ -1930,8 +1910,7 @@ bool cpp_typecheckt::static_typecast( e.type().id()==ID_unsignedbv || e.type().id()==ID_c_enum_tag)) { - new_expr=e; - new_expr.make_typecast(type); + new_expr = typecast_exprt::conditional_cast(e, type); new_expr.remove(ID_C_lvalue); return true; } @@ -1966,9 +1945,8 @@ bool cpp_typecheckt::static_typecast( if(from.id()==ID_empty) { - e.make_typecast(type); - new_expr.swap(e); - return true; + new_expr = typecast_exprt::conditional_cast(e, type); + return true; } if(to.id()==ID_struct && from.id()==ID_struct) @@ -2007,8 +1985,7 @@ bool cpp_typecheckt::static_typecast( if(subtype_typecast(from_struct, to_struct)) { - new_expr=e; - new_expr.make_typecast(type); + new_expr = typecast_exprt::conditional_cast(e, type); return true; } } diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index 6164164a058..08864cf90b8 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -296,8 +296,8 @@ void cpp_typecheckt::zero_initializer( const unsignedbv_typet enum_type( to_bitvector_type(final_type.subtype()).get_width()); - exprt zero(from_integer(0, enum_type)); - zero.make_typecast(type); + exprt zero = + typecast_exprt::conditional_cast(from_integer(0, enum_type), type); already_typechecked(zero); code_assignt assign; diff --git a/src/cpp/cpp_typecheck_static_assert.cpp b/src/cpp/cpp_typecheck_static_assert.cpp index aa975374bec..30aa476bd20 100644 --- a/src/cpp/cpp_typecheck_static_assert.cpp +++ b/src/cpp/cpp_typecheck_static_assert.cpp @@ -19,7 +19,8 @@ void cpp_typecheckt::convert(cpp_static_assertt &cpp_static_assert) typecheck_expr(cpp_static_assert.op0()); typecheck_expr(cpp_static_assert.op1()); - cpp_static_assert.op0().make_typecast(bool_typet()); + cpp_static_assert.op0() = + typecast_exprt::conditional_cast(cpp_static_assert.op0(), bool_typet()); make_constant(cpp_static_assert.op0()); if(cpp_static_assert.op0().is_true()) diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index 5f9b8caccc2..5dae0bb428c 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -576,8 +576,7 @@ int linker_script_merget::ls_data2instructions( unsigned_int_type().get_width()), unsigned_int_type()); - exprt rhs_tc(rhs); - rhs_tc.make_typecast(pointer_type(char_type())); + typecast_exprt rhs_tc(rhs, pointer_type(char_type())); linker_values.emplace( irep_idt(d["sym"].value), std::make_pair(lhs, rhs_tc)); @@ -640,8 +639,8 @@ int linker_script_merget::ls_data2instructions( string2integer(d["val"].value), unsigned_int_type().get_width())); rhs.type()=unsigned_int_type(); - exprt rhs_tc(rhs); - rhs_tc.make_typecast(pointer_type(char_type())); + exprt rhs_tc = + typecast_exprt::conditional_cast(rhs, pointer_type(char_type())); linker_values.emplace( irep_idt(d["sym"].value), std::make_pair(lhs, rhs_tc)); diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index ec22532502c..7243c40c446 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -1846,7 +1846,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast) const typet &t=expr.type(); - expr.make_typecast(t); + expr = typecast_exprt(expr, t); add_local_types(t); const irep_idt &typedef_str=expr.type().get(ID_C_typedef); @@ -1944,10 +1944,10 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast) else if(expr.type().id()==ID_bool || expr.type().id()==ID_c_bool) { - expr=from_integer( - expr.is_true()?1:0, - signedbv_typet(config.ansi_c.int_width)); - expr.make_typecast(bool_typet()); + expr = typecast_exprt( + from_integer( + expr.is_true() ? 1 : 0, signedbv_typet(config.ansi_c.int_width)), + bool_typet()); } const irept &c_sizeof_type=expr.find(ID_C_c_sizeof_type); diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 82bbce148ac..2bacd9cfdda 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -441,10 +441,8 @@ void goto_convertt::do_cpp_new( if(new_array) { - count=static_cast(rhs.find(ID_size)); - - if(count.type()!=object_size.type()) - count.make_typecast(object_size.type()); + count = typecast_exprt::conditional_cast( + static_cast(rhs.find(ID_size)), object_size.type()); // might have side-effect clean_expr(count, dest, ID_cpp); @@ -513,8 +511,10 @@ void goto_convertt::do_cpp_new( new_call.add_source_location()=rhs.source_location(); for(std::size_t i=0; isource_location.set("user-provided", true); // let's double-check the type of the argument - if(t->guard.type().id()!=ID_bool) - t->guard.make_typecast(bool_typet()); + t->guard = typecast_exprt::conditional_cast(t->guard, bool_typet()); if(lhs.is_not_nil()) { @@ -749,8 +748,7 @@ void goto_convertt::do_function_call_symbol( "assertion " + id2string(from_expr(ns, identifier, t->guard))); // let's double-check the type of the argument - if(t->guard.type().id()!=ID_bool) - t->guard.make_typecast(bool_typet()); + t->guard = typecast_exprt::conditional_cast(t->guard, bool_typet()); if(lhs.is_not_nil()) { @@ -795,8 +793,7 @@ void goto_convertt::do_function_call_symbol( t->source_location.set_comment(description); // let's double-check the type of the argument - if(t->guard.type().id()!=ID_bool) - t->guard.make_typecast(bool_typet()); + t->guard = typecast_exprt::conditional_cast(t->guard, bool_typet()); if(lhs.is_not_nil()) { @@ -1250,8 +1247,8 @@ void goto_convertt::do_function_call_symbol( goto_programt::targett t2=dest.add_instruction(ASSIGN); t2->source_location=function.source_location(); t2->code=code_assignt(lhs, deref_ptr); - if(t2->code.op0().type()!=t2->code.op1().type()) - t2->code.op1().make_typecast(t2->code.op0().type()); + t2->code.op1() = + typecast_exprt::conditional_cast(t2->code.op1(), t2->code.op0().type()); } irep_idt op_id= @@ -1264,9 +1261,11 @@ void goto_convertt::do_function_call_symbol( ID_nil; // build *ptr=*ptr OP arguments[1]; - binary_exprt op_expr(deref_ptr, op_id, arguments[1], deref_ptr.type()); - if(op_expr.op1().type()!=op_expr.type()) - op_expr.op1().make_typecast(op_expr.type()); + binary_exprt op_expr( + deref_ptr, + op_id, + typecast_exprt::conditional_cast(arguments[1], deref_ptr.type()), + deref_ptr.type()); goto_programt::targett t3=dest.add_instruction(ASSIGN); t3->source_location=function.source_location(); @@ -1323,9 +1322,11 @@ void goto_convertt::do_function_call_symbol( ID_nil; // build *ptr=*ptr OP arguments[1]; - binary_exprt op_expr(deref_ptr, op_id, arguments[1], deref_ptr.type()); - if(op_expr.op1().type()!=op_expr.type()) - op_expr.op1().make_typecast(op_expr.type()); + binary_exprt op_expr( + deref_ptr, + op_id, + typecast_exprt::conditional_cast(arguments[1], deref_ptr.type()), + deref_ptr.type()); goto_programt::targett t3=dest.add_instruction(ASSIGN); t3->source_location=function.source_location(); @@ -1337,8 +1338,8 @@ void goto_convertt::do_function_call_symbol( goto_programt::targett t2=dest.add_instruction(ASSIGN); t2->source_location=function.source_location(); t2->code=code_assignt(lhs, deref_ptr); - if(t2->code.op0().type()!=t2->code.op1().type()) - t2->code.op1().make_typecast(t2->code.op0().type()); + t2->code.op1() = + typecast_exprt::conditional_cast(t2->code.op1(), t2->code.op0().type()); } // this instruction implies an mfence, i.e., WRfence @@ -1387,9 +1388,9 @@ void goto_convertt::do_function_call_symbol( t1->source_location=function.source_location(); // build *ptr==oldval - equal_exprt equal(deref_ptr, arguments[1]); - if(equal.op1().type()!=equal.op0().type()) - equal.op1().make_typecast(equal.op0().type()); + equal_exprt equal( + deref_ptr, + typecast_exprt::conditional_cast(arguments[1], deref_ptr.type())); if(lhs.is_not_nil()) { @@ -1397,8 +1398,8 @@ void goto_convertt::do_function_call_symbol( goto_programt::targett t2=dest.add_instruction(ASSIGN); t2->source_location=function.source_location(); t2->code=code_assignt(lhs, equal); - if(t2->code.op0().type()!=t2->code.op1().type()) - t2->code.op1().make_typecast(t2->code.op0().type()); + t2->code.op1() = + typecast_exprt::conditional_cast(t2->code.op1(), t2->code.op0().type()); } // build (*ptr==oldval)?newval:*ptr @@ -1453,14 +1454,14 @@ void goto_convertt::do_function_call_symbol( goto_programt::targett t2=dest.add_instruction(ASSIGN); t2->source_location=function.source_location(); t2->code=code_assignt(lhs, deref_ptr); - if(t2->code.op0().type()!=t2->code.op1().type()) - t2->code.op1().make_typecast(t2->code.op0().type()); + t2->code.op1() = + typecast_exprt::conditional_cast(t2->code.op1(), t2->code.op0().type()); } // build *ptr==oldval - equal_exprt equal(deref_ptr, arguments[1]); - if(equal.op1().type()!=equal.op0().type()) - equal.op1().make_typecast(equal.op0().type()); + equal_exprt equal( + deref_ptr, + typecast_exprt::conditional_cast(arguments[1], deref_ptr.type())); // build (*ptr==oldval)?newval:*ptr if_exprt if_expr( @@ -1534,10 +1535,14 @@ void goto_convertt::do_function_call_symbol( if(arguments[0].type()!=arguments[1].type()) { if(use_double) - new_arguments[1].make_typecast(arguments[0].type()); + { + new_arguments[1] = + typecast_exprt(new_arguments[1], arguments[0].type()); + } else { - new_arguments[0].make_typecast(arguments[1].type()); + new_arguments[0] = + typecast_exprt(new_arguments[0], arguments[1].type()); use_double=true; } } diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index f48b1137dcd..5d8abc0b246 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/src/goto-programs/goto_clean_expr.cpp @@ -504,12 +504,13 @@ void goto_convertt::remove_gcc_conditional_expression( clean_expr(expr.op0(), dest, mode); // now we can copy op0 safely - if_exprt if_expr(expr.op0(), expr.op0(), expr.op1(), expr.type()); + if_exprt if_expr( + typecast_exprt::conditional_cast(expr.op0(), bool_typet()), + expr.op0(), + expr.op1(), + expr.type()); if_expr.add_source_location()=expr.source_location(); - if(if_expr.cond().type()!=bool_typet()) - if_expr.cond().make_typecast(bool_typet()); - expr.swap(if_expr); // there might still be junk in expr.op2() diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index adb1ec934cb..a2465b10798 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -506,8 +506,8 @@ void goto_convertt::convert( else if(statement==ID_static_assert) { PRECONDITION(code.operands().size() == 2); - exprt assertion=code.op0(); - assertion.make_typecast(bool_typet()); + exprt assertion = + typecast_exprt::conditional_cast(code.op0(), bool_typet()); simplify(assertion, ns); INVARIANT_WITH_DIAGNOSTICS( !assertion.is_false(), diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index f50b23d62e2..62134244652 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -102,7 +102,7 @@ void goto_inlinet::parameter_assignments( f_acttype.id()==ID_array && f_partype.subtype()==f_acttype.subtype())) { - actual.make_typecast(par_type); + actual = typecast_exprt(actual, par_type); } else if((f_partype.id()==ID_signedbv || f_partype.id()==ID_unsignedbv || @@ -111,7 +111,7 @@ void goto_inlinet::parameter_assignments( f_acttype.id()==ID_unsignedbv || f_acttype.id()==ID_bool)) { - actual.make_typecast(par_type); + actual = typecast_exprt(actual, par_type); } else { @@ -191,15 +191,10 @@ void goto_inlinet::replace_return( continue; } - code_assignt code_assign(lhs, it->code.op0()); - - // this may happen if the declared return type at the call site - // differs from the defined return type - if(code_assign.lhs().type()!= - code_assign.rhs().type()) - code_assign.rhs().make_typecast(code_assign.lhs().type()); - - it->code=code_assign; + // a typecast may be necessary if the declared return type at the call + // site differs from the defined return type + it->code = code_assignt( + lhs, typecast_exprt::conditional_cast(it->code.op0(), lhs.type())); it->type=ASSIGN; it++; diff --git a/src/goto-programs/parameter_assignments.cpp b/src/goto-programs/parameter_assignments.cpp index 2f9ceb31255..13cde49f5ce 100644 --- a/src/goto-programs/parameter_assignments.cpp +++ b/src/goto-programs/parameter_assignments.cpp @@ -72,9 +72,8 @@ void parameter_assignmentst::do_function_calls( t->source_location=i_it->source_location; const symbolt &lhs_symbol=ns.lookup(p_identifier); symbol_exprt lhs=lhs_symbol.symbol_expr(); - exprt rhs=function_call.arguments()[nr]; - if(rhs.type()!=lhs.type()) - rhs.make_typecast(lhs.type()); + exprt rhs = typecast_exprt::conditional_cast( + function_call.arguments()[nr], lhs.type()); t->code=code_assignt(lhs, rhs); } } diff --git a/src/goto-programs/pointer_arithmetic.cpp b/src/goto-programs/pointer_arithmetic.cpp index bc566a21159..a5a427588cc 100644 --- a/src/goto-programs/pointer_arithmetic.cpp +++ b/src/goto-programs/pointer_arithmetic.cpp @@ -72,12 +72,8 @@ void pointer_arithmetict::add_to_offset(const exprt &src) offset.copy_to_operands(src); else { - exprt new_offset=plus_exprt(offset, src); - - if(new_offset.op1().type()!=offset.type()) - new_offset.op1().make_typecast(offset.type()); - - offset=new_offset; + offset = + plus_exprt(offset, typecast_exprt::conditional_cast(src, offset.type())); } } diff --git a/src/goto-programs/printf_formatter.cpp b/src/goto-programs/printf_formatter.cpp index 22cdd25def5..8dcae5894bd 100644 --- a/src/goto-programs/printf_formatter.cpp +++ b/src/goto-programs/printf_formatter.cpp @@ -16,16 +16,14 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include const exprt printf_formattert::make_type( const exprt &src, const typet &dest) { if(src.type()==dest) return src; - exprt tmp=src; - tmp.make_typecast(dest); - simplify(tmp, ns); - return tmp; + return simplify_expr(typecast_exprt(src, dest), ns); } void printf_formattert::operator()( diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 343473b623a..1768c55c2c9 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -217,7 +217,8 @@ void remove_function_pointerst::fix_argument_types( if(!type_eq(call_arguments[i].type(), function_parameters[i].type(), ns)) { - call_arguments[i].make_typecast(function_parameters[i].type()); + call_arguments[i] = + typecast_exprt(call_arguments[i], function_parameters[i].type()); } } } diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 62c51152c3a..dd05c53e447 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -641,8 +641,9 @@ exprt string_abstractiont::build( if(what==whatt::LENGTH || what==whatt::SIZE) { // adjust for offset - result=minus_exprt(result, pointer_offset(pointer)); - result.op0().make_typecast(result.op1().type()); + exprt offset = pointer_offset(pointer); + result = minus_exprt( + typecast_exprt::conditional_cast(result, offset.type()), offset); } return result; diff --git a/src/goto-programs/string_abstraction.h b/src/goto-programs/string_abstraction.h index ec025846c5b..8b1fa464aa5 100644 --- a/src/goto-programs/string_abstraction.h +++ b/src/goto-programs/string_abstraction.h @@ -65,7 +65,7 @@ class string_abstractiont:public messaget { if(dest.is_not_nil() && ns.follow(dest.type())!=ns.follow(type)) - dest.make_typecast(type); + dest = typecast_exprt(dest, type); } goto_programt::targett abstract( diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp index f32cf4fda05..9aa7cd51a59 100644 --- a/src/goto-programs/string_instrumentation.cpp +++ b/src/goto-programs/string_instrumentation.cpp @@ -74,7 +74,7 @@ class string_instrumentationt:public messaget void make_type(exprt &dest, const typet &type) { if(ns.follow(dest.type())!=ns.follow(type)) - dest.make_typecast(type); + dest = typecast_exprt(dest, type); } void instrument(goto_programt &dest, goto_programt::targett it); diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 2b6bf87edc0..8cc1217f7ea 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -269,8 +269,7 @@ void goto_symext::symex_assign_typecast( assignment_typet assignment_type) { // these may come from dereferencing on the lhs - exprt rhs_typecasted=rhs; - rhs_typecasted.make_typecast(lhs.op().type()); + exprt rhs_typecasted = typecast_exprt::conditional_cast(rhs, lhs.op().type()); exprt new_full_lhs=add_to_lhs(full_lhs, lhs); diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 9a54375bdf5..fcaeedbb2ed 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -198,10 +198,9 @@ void goto_symext::symex_allocate( value_symbol.symbol_expr(), pointer_type(value_symbol.type)); } - if(rhs.type()!=lhs.type()) - rhs.make_typecast(lhs.type()); - - symex_assign(state, code_assignt(lhs, rhs)); + symex_assign( + state, + code_assignt(lhs, typecast_exprt::conditional_cast(rhs, lhs.type()))); } irep_idt get_symbol(const exprt &src) @@ -260,8 +259,8 @@ void goto_symext::symex_gcc_builtin_va_arg_next( if(!ns.lookup(id, symbol)) { const symbol_exprt symbol_expr(symbol->name, symbol->type); - rhs=address_of_exprt(symbol_expr); - rhs.make_typecast(lhs.type()); + rhs = typecast_exprt::conditional_cast( + address_of_exprt(symbol_expr), lhs.type()); } } } diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp index ac95c8a9158..c8522dabd15 100644 --- a/src/goto-symex/symex_clean_expr.cpp +++ b/src/goto-symex/symex_clean_expr.cpp @@ -99,12 +99,10 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns) const typet &array_size_type = prev_array_type.size().type(); const typet &subtype = prev_array_type.subtype(); - exprt new_offset(ode.offset()); - if(new_offset.type() != array_size_type) - new_offset.make_typecast(array_size_type); - exprt subtype_size = size_of_expr(subtype, ns); - if(subtype_size.type() != array_size_type) - subtype_size.make_typecast(array_size_type); + exprt new_offset = + typecast_exprt::conditional_cast(ode.offset(), array_size_type); + exprt subtype_size = typecast_exprt::conditional_cast( + size_of_expr(subtype, ns), array_size_type); new_offset = div_exprt(new_offset, subtype_size); minus_exprt new_size(prev_array_type.size(), new_offset); if(do_simplify) diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp index ad5fb0ff0c6..0a712bde2c1 100644 --- a/src/goto-symex/symex_other.cpp +++ b/src/goto-symex/symex_other.cpp @@ -218,7 +218,7 @@ void goto_symext::symex_other( const array_typet &array_type = to_array_type(array_expr.type()); if(!base_type_eq(array_type.subtype(), value.type(), ns)) - value.make_typecast(array_type.subtype()); + value = typecast_exprt(value, array_type.subtype()); code_assignt assignment(array_expr, array_of_exprt(value, array_type)); symex_assign(state, assignment); diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index b9bf08d6efa..4031d90b70e 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -1089,7 +1089,10 @@ void value_sett::get_reference_set_rec( { // adjust type? if(ns.follow(struct_op.type())!=final_object_type) - member_expr.compound().make_typecast(struct_op.type()); + { + member_expr.compound() = + typecast_exprt(member_expr.compound(), struct_op.type()); + } insert(dest, member_expr, o); } diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 4b203cc77c5..b70ee7bb0ed 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -379,12 +379,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( if(o.offset().is_zero()) { - equal_exprt equality(pointer_expr, object_pointer); - - if(ns.follow(equality.lhs().type())!=ns.follow(equality.rhs().type())) - equality.lhs().make_typecast(equality.rhs().type()); - - result.pointer_guard=equality; + result.pointer_guard = equal_exprt( + typecast_exprt::conditional_cast(pointer_expr, object_pointer.type()), + object_pointer); } else { @@ -446,13 +443,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( // TODO: need to assert well-alignedness } - index_exprt index_expr= - index_exprt(root_object, adjusted_offset, root_object_type.subtype()); - - result.value=index_expr; - - if(ns.follow(result.value.type())!=ns.follow(dereference_type)) - result.value.make_typecast(dereference_type); + result.value = typecast_exprt::conditional_cast( + index_exprt(root_object, adjusted_offset, root_object_type.subtype()), + dereference_type); } else { @@ -589,12 +582,9 @@ bool value_set_dereferencet::memory_model_bytes( *to_type_size == 1 && is_a_bv_type(from_type.subtype()) && is_a_bv_type(to_type)) { - // yes, can use 'index' - result = index_exprt(value, offset, from_type.subtype()); - - // possibly need to convert - if(!base_type_eq(result.type(), to_type, ns)) - result.make_typecast(to_type); + // yes, can use 'index', but possibly need to convert + result = typecast_exprt::conditional_cast( + index_exprt(value, offset, from_type.subtype()), to_type); } else { diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index 7fe898ca3bc..58ec4e51d9c 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -914,7 +914,10 @@ void value_set_fit::get_reference_set_sharing_rec( // adjust type? if(ns.follow(struct_op.type())!=ns.follow(object.type())) - member_expr.compound().make_typecast(struct_op.type()); + { + member_expr.compound() = + typecast_exprt(member_expr.compound(), struct_op.type()); + } insert(dest, member_expr, o); } diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp index 64de09c84b6..b13aa2da58b 100644 --- a/src/pointer-analysis/value_set_fivr.cpp +++ b/src/pointer-analysis/value_set_fivr.cpp @@ -1027,7 +1027,10 @@ void value_set_fivrt::get_reference_set_sharing_rec( // adjust type? if(ns.follow(struct_op.type())!=ns.follow(object.type())) - member_expr.compound().make_typecast(struct_op.type()); + { + member_expr.compound() = + typecast_exprt(member_expr.compound(), struct_op.type()); + } insert_from(dest, member_expr, o); } diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp index 4d6ee509c24..9ea66c0f2bc 100644 --- a/src/pointer-analysis/value_set_fivrns.cpp +++ b/src/pointer-analysis/value_set_fivrns.cpp @@ -720,7 +720,10 @@ void value_set_fivrnst::get_reference_set_rec( // adjust type? if(ns.follow(struct_op.type())!=ns.follow(object.type())) - member_expr.compound().make_typecast(struct_op.type()); + { + member_expr.compound() = + typecast_exprt(member_expr.compound(), struct_op.type()); + } insert_from(dest, member_expr, o); } diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index 227283f6e6b..83f52bc5af8 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -600,8 +600,7 @@ void arrayst::add_array_constraints_update( { // we first build the guard - if(other_index.type()!=index.type()) - other_index.make_typecast(index.type()); + other_index = typecast_exprt::conditional_cast(other_index, index.type()); literalt guard_lit=convert(equal_exprt(index, other_index));