File tree 1 file changed +0
-35
lines changed 1 file changed +0
-35
lines changed Original file line number Diff line number Diff line change @@ -170,41 +170,6 @@ literalt boolbvt::convert_overflow(const exprt &expr)
170
170
171
171
return bv_utils.overflow_negate (bv);
172
172
}
173
- else if (has_prefix (expr.id_string (), " overflow-typecast-" ))
174
- {
175
- std::size_t bits=unsafe_string2unsigned (id2string (expr.id ()).substr (18 ));
176
- INVARIANT (bits != 0 , " " );
177
-
178
- const exprt::operandst &operands=expr.operands ();
179
-
180
- DATA_INVARIANT (
181
- operands.size () == 1 ,
182
- " expression " + expr.id_string () + " should have one operand" );
183
-
184
- const exprt &op=operands[0 ];
185
-
186
- const bvt &bv=convert_bv (op);
187
-
188
- INVARIANT (bits < bv.size (), " " );
189
-
190
- // signed or unsigned?
191
- if (op.type ().id ()==ID_signedbv)
192
- {
193
- bvt tmp_bv;
194
- for (std::size_t i=bits; i<bv.size (); i++)
195
- tmp_bv.push_back (prop.lxor (bv[bits-1 ], bv[i]));
196
-
197
- return prop.lor (tmp_bv);
198
- }
199
- else
200
- {
201
- bvt tmp_bv;
202
- for (std::size_t i=bits; i<bv.size (); i++)
203
- tmp_bv.push_back (bv[i]);
204
-
205
- return prop.lor (tmp_bv);
206
- }
207
- }
208
173
209
174
return SUB::convert_rest (expr);
210
175
}
You can’t perform that action at this time.
0 commit comments