Skip to content

Commit 9f92ab9

Browse files
committed
Move LHS type casts to RHS in assign_* instructions
Doing so during goto-program conversion will ensure we can generate appropriate conversion checks. Fixes: #4208
1 parent 2f1bb0f commit 9f92ab9

File tree

2 files changed

+6
-2
lines changed

2 files changed

+6
-2
lines changed

regression/cbmc/Overflow_Addition3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--signed-overflow-check --conversion-check
44
^EXIT=10$

src/goto-programs/goto_convert_side_effect.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -107,7 +107,11 @@ void goto_convertt::remove_assignment(
107107
rhs.type() = expr.op0().type();
108108
rhs.add_source_location() = expr.source_location();
109109

110-
code_assignt assignment(expr.op0(), rhs);
110+
exprt new_lhs = skip_typecast(expr.op0());
111+
rhs = typecast_exprt::conditional_cast(rhs, new_lhs.type());
112+
rhs.add_source_location() = expr.source_location();
113+
114+
code_assignt assignment(new_lhs, rhs);
111115
assignment.add_source_location()=expr.source_location();
112116

113117
convert(assignment, dest, mode);

0 commit comments

Comments
 (0)