Skip to content

Commit f0fbf4b

Browse files
committed
Use complex_real_exprt and complex_imag_exprt in goto symex
1 parent 661c08a commit f0fbf4b

File tree

1 file changed

+22
-17
lines changed

1 file changed

+22
-17
lines changed

src/goto-symex/symex_assign.cpp

Lines changed: 22 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -168,28 +168,33 @@ void goto_symext::symex_assign_rec(
168168
symex_assign_byte_extract(
169169
state, to_byte_extract_expr(lhs), full_lhs, rhs, guard, assignment_type);
170170
}
171-
else if(lhs.id()==ID_complex_real ||
172-
lhs.id()==ID_complex_imag)
171+
else if(lhs.id() == ID_complex_real)
173172
{
174-
// this is stuff like __real__ x = 1;
175-
assert(lhs.operands().size()==1);
173+
const complex_real_exprt &complex_real_expr = to_complex_real_expr(lhs);
176174

177-
exprt new_rhs=exprt(ID_complex, lhs.op0().type());
178-
new_rhs.operands().resize(2);
175+
const complex_imag_exprt complex_imag_expr(complex_real_expr.op());
179176

180-
if(lhs.id()==ID_complex_real)
181-
{
182-
new_rhs.op0()=rhs;
183-
new_rhs.op1()=unary_exprt(ID_complex_imag, lhs.op0(), lhs.type());
184-
}
185-
else
186-
{
187-
new_rhs.op0()=unary_exprt(ID_complex_real, lhs.op0(), lhs.type());
188-
new_rhs.op1()=rhs;
189-
}
177+
complex_exprt new_rhs(
178+
rhs,
179+
complex_imag_expr,
180+
to_complex_type(complex_real_expr.op().type()));
181+
182+
symex_assign_rec(
183+
state, complex_real_expr.op(), full_lhs, new_rhs, guard, assignment_type);
184+
}
185+
else if(lhs.id() == ID_complex_imag)
186+
{
187+
const complex_imag_exprt &complex_imag_expr = to_complex_imag_expr(lhs);
188+
189+
const complex_real_exprt complex_real_expr(complex_imag_expr.op());
190+
191+
complex_exprt new_rhs(
192+
complex_real_expr,
193+
rhs,
194+
to_complex_type(complex_imag_expr.op().type()));
190195

191196
symex_assign_rec(
192-
state, lhs.op0(), full_lhs, new_rhs, guard, assignment_type);
197+
state, complex_imag_expr.op(), full_lhs, new_rhs, guard, assignment_type);
193198
}
194199
else
195200
throw "assignment to `"+lhs.id_string()+"' not handled";

0 commit comments

Comments
 (0)