File tree 1 file changed +4
-6
lines changed
1 file changed +4
-6
lines changed Original file line number Diff line number Diff line change @@ -362,9 +362,9 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
362
362
if (it->type ().id ()!=ID_unsignedbv &&
363
363
it->type ().id ()!=ID_signedbv)
364
364
{
365
- bvt bv ;
366
- conversion_failed (plus_expr, bv );
367
- return bv ;
365
+ bvt failed_bv ;
366
+ conversion_failed (plus_expr, failed_bv );
367
+ return failed_bv ;
368
368
}
369
369
370
370
bv_utilst::representationt rep=
@@ -398,8 +398,6 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
398
398
minus_expr.op0 ().type ().id () == ID_pointer,
399
399
" first operand should be of pointer type" );
400
400
401
- bvt bv;
402
-
403
401
if (
404
402
minus_expr.op1 ().type ().id () != ID_unsignedbv &&
405
403
minus_expr.op1 ().type ().id () != ID_signedbv)
@@ -411,7 +409,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
411
409
412
410
const unary_minus_exprt neg_op1 (minus_expr.op1 ());
413
411
414
- bv = convert_bv (minus_expr.op0 ());
412
+ bvt bv = convert_bv (minus_expr.op0 ());
415
413
416
414
typet pointer_sub_type = minus_expr.op0 ().type ().subtype ();
417
415
mp_integer element_size;
You can’t perform that action at this time.
0 commit comments