Skip to content

Commit e254a6f

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 6ff951c commit e254a6f

File tree

2 files changed

+13
-6
lines changed

2 files changed

+13
-6
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: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -44,10 +44,13 @@ void goto_convertt::remove_assignment(
4444

4545
if(statement==ID_assign)
4646
{
47-
exprt tmp=expr;
48-
tmp.id(ID_code);
49-
// just interpret as code
50-
convert_assign(to_code_assign(to_code(tmp)), dest, mode);
47+
exprt new_lhs = skip_typecast(expr.op0());
48+
exprt new_rhs =
49+
typecast_exprt::conditional_cast(expr.op1(), new_lhs.type());
50+
code_assignt assign(std::move(new_lhs), std::move(new_rhs));
51+
assign.add_source_location() = expr.source_location();
52+
53+
convert_assign(assign, dest, mode);
5154
}
5255
else if(statement==ID_assign_plus ||
5356
statement==ID_assign_minus ||
@@ -107,7 +110,11 @@ void goto_convertt::remove_assignment(
107110
rhs.type() = expr.op0().type();
108111
rhs.add_source_location() = expr.source_location();
109112

110-
code_assignt assignment(expr.op0(), rhs);
113+
exprt new_lhs = skip_typecast(expr.op0());
114+
rhs = typecast_exprt::conditional_cast(rhs, new_lhs.type());
115+
rhs.add_source_location() = expr.source_location();
116+
117+
code_assignt assignment(new_lhs, rhs);
111118
assignment.add_source_location()=expr.source_location();
112119

113120
convert(assignment, dest, mode);

0 commit comments

Comments
 (0)