diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index 776729291f4..0569d84de49 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/src/goto-programs/goto_clean_expr.cpp @@ -384,7 +384,7 @@ void goto_convertt::clean_expr( clean_expr(side_effect_assign.lhs(), dest, mode); exprt lhs = side_effect_assign.lhs(); - const bool must_use_rhs = needs_cleaning(lhs); + const bool must_use_rhs = assignment_lhs_needs_temporary(lhs); if(must_use_rhs) { remove_function_call( diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 61317628b7f..103baa005b8 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -89,6 +89,15 @@ class goto_convertt:public messaget static bool needs_cleaning(const exprt &expr); + // Do we need to introduce a temporary for the value of an assignment + // to the given lhs? E.g., a[i] needs a temporary as its value may change + // when i is changed; likewise, *p needs a temporary as its value may change + // when p is changed. + static bool assignment_lhs_needs_temporary(const exprt &lhs) + { + return lhs.id() != ID_symbol; + } + void make_temp_symbol( exprt &expr, const std::string &suffix, diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index 2d94df6a85e..4f045b7f761 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -50,7 +50,9 @@ void goto_convertt::remove_assignment( { auto &old_assignment = to_side_effect_expr_assign(expr); - if(result_is_used && !address_taken && needs_cleaning(old_assignment.lhs())) + if( + result_is_used && !address_taken && + assignment_lhs_needs_temporary(old_assignment.lhs())) { if(!old_assignment.rhs().is_constant()) make_temp_symbol(old_assignment.rhs(), "assign", dest, mode); @@ -122,7 +124,9 @@ void goto_convertt::remove_assignment( exprt rhs = binary_exprt{binary_expr.op0(), new_id, binary_expr.op1()}; rhs.add_source_location() = expr.source_location(); - if(result_is_used && !address_taken && needs_cleaning(binary_expr.op0())) + if( + result_is_used && !address_taken && + assignment_lhs_needs_temporary(binary_expr.op0())) { make_temp_symbol(rhs, "assign", dest, mode); replacement_expr_opt = rhs; @@ -237,7 +241,7 @@ void goto_convertt::remove_pre( } const bool cannot_use_lhs = - result_is_used && !address_taken && needs_cleaning(lhs); + result_is_used && !address_taken && assignment_lhs_needs_temporary(lhs); if(cannot_use_lhs) make_temp_symbol(rhs, "pre", dest, mode);