diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp index c015c1fe414..7d836821870 100644 --- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp +++ b/src/ansi-c/goto-conversion/goto_clean_expr.cpp @@ -114,13 +114,15 @@ void goto_convertt::rewrite_boolean(exprt &expr) "' must be Boolean, but got ", irep_pretty_diagnosticst{expr}); + const source_locationt source_location = expr.find_source_location(); + // re-write "a ==> b" into a?b:1 if(auto implies = expr_try_dynamic_cast(expr)) { expr = if_exprt{ std::move(implies->lhs()), std::move(implies->rhs()), - true_exprt{}, + true_exprt{}.with_source_location(source_location), bool_typet{}}; return; } @@ -135,6 +137,8 @@ void goto_convertt::rewrite_boolean(exprt &expr) else // ID_or tmp = false_exprt(); + tmp.add_source_location() = source_location; + exprt::operandst &ops = expr.operands(); // start with last one @@ -146,17 +150,21 @@ void goto_convertt::rewrite_boolean(exprt &expr) DATA_INVARIANT_WITH_DIAGNOSTICS( op.is_boolean(), "boolean operators must have only boolean operands", - expr.find_source_location()); + source_location); if(expr.id() == ID_and) { - if_exprt if_e(op, tmp, false_exprt()); + exprt if_e = + if_exprt{op, tmp, false_exprt{}.with_source_location(source_location)} + .with_source_location(source_location); tmp.swap(if_e); continue; } if(expr.id() == ID_or) { - if_exprt if_e(op, true_exprt(), tmp); + exprt if_e = + if_exprt{op, true_exprt{}.with_source_location(source_location), tmp} + .with_source_location(source_location); tmp.swap(if_e); continue; } diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 7db4f3456b7..1be6140690e 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -236,11 +236,11 @@ static void fix_return_type( exprt old_lhs=function_call.lhs(); function_call.lhs()=tmp_symbol_expr; - dest.add(goto_programt::make_assignment(code_assignt( + dest.add(goto_programt::make_assignment( old_lhs, make_byte_extract( tmp_symbol_expr, from_integer(0, c_index_type()), old_lhs.type()), - source_location))); + source_location)); } void remove_function_pointerst::remove_function_pointer(