@@ -92,9 +92,12 @@ void rw_range_sett::get_objects_complex(
92
92
const exprt &op=expr.op0 ();
93
93
assert (op.type ().id ()==ID_complex);
94
94
95
- range_spect sub_size=
96
- to_range_spect (pointer_offset_bits (op.type ().subtype (), ns));
97
- assert (sub_size>0 );
95
+ auto subtype_bits = pointer_offset_bits (op.type ().subtype (), ns);
96
+ CHECK_RETURN (subtype_bits.has_value ());
97
+
98
+ range_spect sub_size = to_range_spect (*subtype_bits);
99
+ CHECK_RETURN (sub_size > 0 );
100
+
98
101
range_spect offset=
99
102
(range_start==-1 || expr.id ()==ID_complex_real) ? 0 : sub_size;
100
103
@@ -167,8 +170,9 @@ void rw_range_sett::get_objects_shift(
167
170
{
168
171
const exprt simp_distance=simplify_expr (shift.distance (), ns);
169
172
170
- range_spect src_size=
171
- to_range_spect (pointer_offset_bits (shift.op ().type (), ns));
173
+ auto op_bits = pointer_offset_bits (shift.op ().type (), ns);
174
+
175
+ range_spect src_size = op_bits.has_value () ? to_range_spect (*op_bits) : -1 ;
172
176
173
177
mp_integer dist;
174
178
if (range_start==-1 ||
@@ -224,15 +228,18 @@ void rw_range_sett::get_objects_member(
224
228
225
229
const struct_typet &struct_type=to_struct_type (type);
226
230
227
- range_spect offset=
228
- to_range_spect (
229
- member_offset_bits (
230
- struct_type,
231
- expr.get_component_name (),
232
- ns));
231
+ auto offset_bits =
232
+ member_offset_bits (struct_type, expr.get_component_name (), ns);
233
233
234
- if (offset!=-1 )
235
- offset+=range_start;
234
+ range_spect offset;
235
+
236
+ if (offset_bits.has_value ())
237
+ {
238
+ offset = to_range_spect (*offset_bits);
239
+ offset += range_start;
240
+ }
241
+ else
242
+ offset = -1 ;
236
243
237
244
get_objects_rec (mode, expr.struct_op (), offset, size);
238
245
}
@@ -253,15 +260,17 @@ void rw_range_sett::get_objects_index(
253
260
{
254
261
const vector_typet &vector_type=to_vector_type (type);
255
262
256
- sub_size=
257
- to_range_spect (pointer_offset_bits (vector_type.subtype (), ns));
263
+ auto subtype_bits = pointer_offset_bits (vector_type.subtype (), ns);
264
+
265
+ sub_size = subtype_bits.has_value () ? to_range_spect (*subtype_bits) : -1 ;
258
266
}
259
267
else if (type.id ()==ID_array)
260
268
{
261
269
const array_typet &array_type=to_array_type (type);
262
270
263
- sub_size=
264
- to_range_spect (pointer_offset_bits (array_type.subtype (), ns));
271
+ auto subtype_bits = pointer_offset_bits (array_type.subtype (), ns);
272
+
273
+ sub_size = subtype_bits.has_value () ? to_range_spect (*subtype_bits) : -1 ;
265
274
}
266
275
else
267
276
return ;
@@ -296,10 +305,13 @@ void rw_range_sett::get_objects_array(
296
305
const array_typet &array_type=
297
306
to_array_type (ns.follow (expr.type ()));
298
307
299
- range_spect sub_size=
300
- to_range_spect (pointer_offset_bits (array_type.subtype (), ns));
308
+ auto subtype_bits = pointer_offset_bits (array_type.subtype (), ns);
301
309
302
- if (sub_size==-1 )
310
+ range_spect sub_size;
311
+
312
+ if (subtype_bits.has_value ())
313
+ sub_size = to_range_spect (*subtype_bits);
314
+ else
303
315
{
304
316
forall_operands (it, expr)
305
317
get_objects_rec (mode, *it, 0 , -1 );
@@ -336,17 +348,20 @@ void rw_range_sett::get_objects_struct(
336
348
const struct_typet &struct_type=
337
349
to_struct_type (ns.follow (expr.type ()));
338
350
339
- range_spect full_size=
340
- to_range_spect (pointer_offset_bits (struct_type, ns));
351
+ auto struct_bits = pointer_offset_bits (struct_type, ns);
352
+
353
+ range_spect full_size =
354
+ struct_bits.has_value () ? to_range_spect (*struct_bits) : -1 ;
341
355
342
356
range_spect offset=0 ;
343
357
range_spect full_r_s=range_start==-1 ? 0 : range_start;
344
358
range_spect full_r_e=size==-1 || full_size==-1 ? -1 : full_r_s+size;
345
359
346
360
forall_operands (it, expr)
347
361
{
348
- range_spect sub_size=
349
- to_range_spect (pointer_offset_bits (it->type (), ns));
362
+ auto it_bits = pointer_offset_bits (it->type (), ns);
363
+
364
+ range_spect sub_size = it_bits.has_value () ? to_range_spect (*it_bits) : -1 ;
350
365
351
366
if (offset==-1 )
352
367
{
@@ -395,8 +410,9 @@ void rw_range_sett::get_objects_typecast(
395
410
{
396
411
const exprt &op=tc.op ();
397
412
398
- range_spect new_size=
399
- to_range_spect (pointer_offset_bits (op.type (), ns));
413
+ auto op_bits = pointer_offset_bits (op.type (), ns);
414
+
415
+ range_spect new_size = op_bits.has_value () ? to_range_spect (*op_bits) : -1 ;
400
416
401
417
if (range_start==-1 )
402
418
new_size=-1 ;
@@ -528,8 +544,11 @@ void rw_range_sett::get_objects_rec(
528
544
{
529
545
const symbol_exprt &symbol=to_symbol_expr (expr);
530
546
const irep_idt identifier=symbol.get_identifier ();
531
- range_spect full_size=
532
- to_range_spect (pointer_offset_bits (symbol.type (), ns));
547
+
548
+ auto symbol_bits = pointer_offset_bits (symbol.type (), ns);
549
+
550
+ range_spect full_size =
551
+ symbol_bits.has_value () ? to_range_spect (*symbol_bits) : -1 ;
533
552
534
553
if (full_size==0 ||
535
554
(full_size>0 && range_start>=full_size))
@@ -575,8 +594,10 @@ void rw_range_sett::get_objects_rec(
575
594
576
595
void rw_range_sett::get_objects_rec (get_modet mode, const exprt &expr)
577
596
{
578
- range_spect size=
579
- to_range_spect (pointer_offset_bits (expr.type (), ns));
597
+ auto expr_bits = pointer_offset_bits (expr.type (), ns);
598
+
599
+ range_spect size = expr_bits.has_value () ? to_range_spect (*expr_bits) : -1 ;
600
+
580
601
get_objects_rec (mode, expr, 0 , size);
581
602
}
582
603
@@ -605,16 +626,24 @@ void rw_range_set_value_sett::get_objects_dereference(
605
626
exprt object=deref;
606
627
dereference (target, object, ns, value_sets);
607
628
608
- range_spect new_size=
609
- to_range_spect (pointer_offset_bits (object.type (), ns));
629
+ auto type_bits = pointer_offset_bits (object.type (), ns);
610
630
611
- if (range_start==- 1 || new_size<=range_start)
612
- new_size=- 1 ;
613
- else
631
+ range_spect new_size;
632
+
633
+ if (type_bits. has_value ())
614
634
{
615
- new_size-=range_start;
616
- new_size=std::min (size, new_size);
635
+ new_size = to_range_spect (*type_bits);
636
+
637
+ if (range_start == -1 || new_size <= range_start)
638
+ new_size = -1 ;
639
+ else
640
+ {
641
+ new_size -= range_start;
642
+ new_size = std::min (size, new_size);
643
+ }
617
644
}
645
+ else
646
+ new_size = -1 ;
618
647
619
648
// value_set_dereferencet::build_reference_to will turn *p into
620
649
// DYNAMIC_OBJECT(p) ? *p : invalid_objectN
0 commit comments