diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index b852bb16100..3f363ea9cd7 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -1673,8 +1673,8 @@ void c_typecheck_baset::typecheck_side_effect_gcc_conditional_expression( typecheck_expr_trinary(if_expr); // copy the result - expr.op0()=if_expr.op1(); - expr.op1()=if_expr.op2(); + expr.op0() = if_expr.true_case(); + expr.op1() = if_expr.false_case(); expr.type()=if_expr.type(); } diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 19ab944b0a0..82bbce148ac 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -1402,9 +1402,11 @@ void goto_convertt::do_function_call_symbol( } // build (*ptr==oldval)?newval:*ptr - if_exprt if_expr(equal, arguments[2], deref_ptr, deref_ptr.type()); - if(if_expr.op1().type()!=if_expr.type()) - if_expr.op1().make_typecast(if_expr.type()); + if_exprt if_expr( + equal, + typecast_exprt::conditional_cast(arguments[2], deref_ptr.type()), + deref_ptr, + deref_ptr.type()); goto_programt::targett t3=dest.add_instruction(ASSIGN); t3->source_location=function.source_location(); @@ -1461,9 +1463,11 @@ void goto_convertt::do_function_call_symbol( equal.op1().make_typecast(equal.op0().type()); // build (*ptr==oldval)?newval:*ptr - if_exprt if_expr(equal, arguments[2], deref_ptr, deref_ptr.type()); - if(if_expr.op1().type()!=if_expr.type()) - if_expr.op1().make_typecast(if_expr.type()); + if_exprt if_expr( + equal, + typecast_exprt::conditional_cast(arguments[2], deref_ptr.type()), + deref_ptr, + deref_ptr.type()); goto_programt::targett t3=dest.add_instruction(ASSIGN); t3->source_location=function.source_location(); diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp index a2c6c376d9a..44a130302b3 100644 --- a/src/solvers/lowering/byte_operators.cpp +++ b/src/solvers/lowering/byte_operators.cpp @@ -362,9 +362,9 @@ static exprt lower_byte_update( const mp_integer &element_size = *element_size_opt; - if(src.op0().type().id()==ID_array) + if(src.op().type().id()==ID_array) { - const array_typet &array_type=to_array_type(src.op0().type()); + const array_typet &array_type=to_array_type(src.op().type()); const typet &subtype=array_type.subtype(); // array of bitvectors? @@ -531,14 +531,14 @@ static exprt lower_byte_update( subtype.id_string()); } } - else if(src.op0().type().id()==ID_signedbv || - src.op0().type().id()==ID_unsignedbv || - src.op0().type().id()==ID_floatbv || - src.op0().type().id()==ID_c_bool || - src.op0().type().id()==ID_pointer) + else if(src.op().type().id()==ID_signedbv || + src.op().type().id()==ID_unsignedbv || + src.op().type().id()==ID_floatbv || + src.op().type().id()==ID_c_bool || + src.op().type().id()==ID_pointer) { // do a shift, mask and OR - const auto type_width = pointer_offset_bits(src.op0().type(), ns); + const auto type_width = pointer_offset_bits(src.op().type(), ns); CHECK_RETURN(type_width.has_value() && *type_width > 0); const std::size_t width = numeric_cast_v(*type_width); @@ -560,7 +560,7 @@ static exprt lower_byte_update( unsignedbv_typet( width - numeric_cast_v(element_size) * 8)), src.value(), - src.op0().type()); + src.op().type()); else value_extended = src.value(); @@ -602,7 +602,7 @@ static exprt lower_byte_update( PRECONDITION_WITH_DIAGNOSTICS( false, "flatten_byte_update can only do arrays and scalars right now", - src.op0().type().id_string()); + src.op().type().id_string()); } } diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 02ba69ccb67..1297de26158 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2061,8 +2061,8 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr) plus_exprt new_offset(offset, compo_offset); simplify_node(new_offset); exprt new_value(with.new_value()); - expr.op1().swap(new_offset); - expr.op2().swap(new_value); + expr.offset().swap(new_offset); + expr.value().swap(new_value); simplify_byte_update(expr); // do this recursively return false; } @@ -2088,8 +2088,8 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr) plus_exprt new_offset(offset, index_offset); simplify_node(new_offset); exprt new_value(with.new_value()); - expr.op1().swap(new_offset); - expr.op2().swap(new_value); + expr.offset().swap(new_offset); + expr.value().swap(new_value); simplify_byte_update(expr); // do this recursively return false; }