Skip to content

Commit 6537914

Browse files
Cleanup invariants in remove_complex
1 parent 4671632 commit 6537914

File tree

1 file changed

+38
-34
lines changed

1 file changed

+38
-34
lines changed

src/goto-programs/remove_complex.cpp

Lines changed: 38 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -32,10 +32,9 @@ static exprt complex_member(const exprt &expr, irep_idt id)
3232
}
3333
else
3434
{
35-
assert(expr.type().id()==ID_struct);
3635
const struct_typet &struct_type=
3736
to_struct_type(expr.type());
38-
assert(struct_type.components().size()==2);
37+
PRECONDITION(struct_type.components().size() == 2);
3938
return member_exprt(expr, id, struct_type.components().front().type());
4039
}
4140
}
@@ -105,20 +104,22 @@ static void remove_complex(exprt &expr)
105104

106105
if(expr.id()==ID_typecast)
107106
{
108-
assert(expr.operands().size()==1);
109-
if(expr.op0().type().id()==ID_complex)
107+
auto const &typecast_expr = to_typecast_expr(expr);
108+
if(typecast_expr.op().type().id() == ID_complex)
110109
{
111-
if(expr.type().id()==ID_complex)
110+
if(typecast_expr.type().id() == ID_complex)
112111
{
113112
// complex to complex
114113
}
115114
else
116115
{
117116
// cast complex to non-complex is (T)__real__ x
118117
unary_exprt tmp(
119-
ID_complex_real, expr.op0(), expr.op0().type().subtype());
118+
ID_complex_real,
119+
typecast_expr.op(),
120+
typecast_expr.op().type().subtype());
120121

121-
expr=typecast_exprt(tmp, expr.type());
122+
expr = typecast_exprt(tmp, typecast_expr.type());
122123
}
123124
}
124125
}
@@ -131,7 +132,8 @@ static void remove_complex(exprt &expr)
131132
if(expr.id()==ID_plus || expr.id()==ID_minus ||
132133
expr.id()==ID_mult || expr.id()==ID_div)
133134
{
134-
assert(expr.operands().size()==2);
135+
DATA_INVARIANT(
136+
expr.operands().size() == 2, "binary operators have 2 arguments");
135137
// do component-wise:
136138
// x+y -> complex(x.r+y.r,x.i+y.i)
137139
struct_exprt struct_expr(expr.type());
@@ -153,62 +155,66 @@ static void remove_complex(exprt &expr)
153155
}
154156
else if(expr.id()==ID_unary_minus)
155157
{
156-
assert(expr.operands().size()==1);
158+
auto const &unary_minus_expr = to_unary_minus_expr(expr);
157159
// do component-wise:
158160
// -x -> complex(-x.r,-x.i)
159-
struct_exprt struct_expr(expr.type());
161+
struct_exprt struct_expr(unary_minus_expr.type());
160162
struct_expr.operands().resize(2);
161163

162-
struct_expr.op0()=
163-
unary_minus_exprt(complex_member(expr.op0(), ID_real));
164+
struct_expr.op0() =
165+
unary_minus_exprt(complex_member(unary_minus_expr.op(), ID_real));
164166

165-
struct_expr.op0().add_source_location()=expr.source_location();
167+
struct_expr.op0().add_source_location() =
168+
unary_minus_expr.source_location();
166169

167-
struct_expr.op1()=
168-
unary_minus_exprt(complex_member(expr.op0(), ID_imag));
170+
struct_expr.op1() =
171+
unary_minus_exprt(complex_member(unary_minus_expr.op(), ID_imag));
169172

170-
struct_expr.op1().add_source_location()=expr.source_location();
173+
struct_expr.op1().add_source_location() =
174+
unary_minus_expr.source_location();
171175

172176
expr=struct_expr;
173177
}
174178
else if(expr.id()==ID_complex)
175179
{
176-
assert(expr.operands().size()==2);
180+
static_cast<void>(to_complex_expr(expr));
177181
expr.id(ID_struct);
178182
}
179183
else if(expr.id()==ID_typecast)
180184
{
181-
assert(expr.operands().size()==1);
182-
typet subtype=expr.type().subtype();
185+
auto const &typecast_expr = to_typecast_expr(expr);
186+
typet subtype = typecast_expr.type().subtype();
183187

184-
if(expr.op0().type().id()==ID_struct)
188+
if(typecast_expr.op().type().id() == ID_struct)
185189
{
186190
// complex to complex -- do typecast per component
187191

188-
struct_exprt struct_expr(expr.type());
192+
struct_exprt struct_expr(typecast_expr.type());
189193
struct_expr.operands().resize(2);
190194

191-
struct_expr.op0()=
192-
typecast_exprt(complex_member(expr.op0(), ID_real), subtype);
195+
struct_expr.op0() =
196+
typecast_exprt(complex_member(typecast_expr.op(), ID_real), subtype);
193197

194-
struct_expr.op0().add_source_location()=expr.source_location();
198+
struct_expr.op0().add_source_location() =
199+
typecast_expr.source_location();
195200

196-
struct_expr.op1()=
197-
typecast_exprt(complex_member(expr.op0(), ID_imag), subtype);
201+
struct_expr.op1() =
202+
typecast_exprt(complex_member(typecast_expr.op(), ID_imag), subtype);
198203

199-
struct_expr.op1().add_source_location()=expr.source_location();
204+
struct_expr.op1().add_source_location() =
205+
typecast_expr.source_location();
200206

201207
expr=struct_expr;
202208
}
203209
else
204210
{
205211
// non-complex to complex
206-
struct_exprt struct_expr(expr.type());
212+
struct_exprt struct_expr(typecast_expr.type());
207213
struct_expr.operands().resize(2);
208214

209-
struct_expr.op0()=typecast_exprt(expr.op0(), subtype);
215+
struct_expr.op0() = typecast_exprt(typecast_expr.op(), subtype);
210216
struct_expr.op1()=from_integer(0, subtype);
211-
struct_expr.add_source_location()=expr.source_location();
217+
struct_expr.add_source_location() = typecast_expr.source_location();
212218

213219
expr=struct_expr;
214220
}
@@ -217,13 +223,11 @@ static void remove_complex(exprt &expr)
217223

218224
if(expr.id()==ID_complex_real)
219225
{
220-
assert(expr.operands().size()==1);
221-
expr=complex_member(expr.op0(), ID_real);
226+
expr = complex_member(to_complex_real_expr(expr).op0(), ID_real);
222227
}
223228
else if(expr.id()==ID_complex_imag)
224229
{
225-
assert(expr.operands().size()==1);
226-
expr=complex_member(expr.op0(), ID_imag);
230+
expr = complex_member(to_complex_imag_expr(expr).op0(), ID_imag);
227231
}
228232

229233
remove_complex(expr.type());

0 commit comments

Comments
 (0)