@@ -206,10 +206,19 @@ exprt symbol_analyzert::get_pointer_to_member_value(
206
206
PRECONDITION (!pointer_value.pointee .empty ());
207
207
208
208
std::string struct_name;
209
- std::string member_offset_string;
210
- split_string (
211
- pointer_value.pointee , ' +' , struct_name, member_offset_string, true );
212
- size_t member_offset = safe_string2size_t (member_offset_string);
209
+ size_t member_offset;
210
+ if (pointer_value.pointee .find (" +" ) != std::string::npos)
211
+ {
212
+ std::string member_offset_string;
213
+ split_string (
214
+ pointer_value.pointee , ' +' , struct_name, member_offset_string, true );
215
+ member_offset = safe_string2size_t (member_offset_string);
216
+ }
217
+ else
218
+ {
219
+ struct_name = pointer_value.pointee ;
220
+ member_offset = 0 ;
221
+ }
213
222
214
223
const symbolt *struct_symbol = symbol_table.lookup (struct_name);
215
224
DATA_INVARIANT (struct_symbol != nullptr , " unknown struct" );
@@ -269,6 +278,24 @@ exprt symbol_analyzert::get_non_char_pointer_value(
269
278
}
270
279
}
271
280
281
+ bool symbol_analyzert::points_to_member (
282
+ const pointer_valuet &pointer_value) const
283
+ {
284
+ if (pointer_value.pointee .find (" +" ) != std::string::npos)
285
+ return true ;
286
+
287
+ const symbolt *pointee_symbol = symbol_table.lookup (pointer_value.pointee );
288
+ if (pointee_symbol == nullptr )
289
+ return false ;
290
+ const auto pointee_type = pointee_symbol->type ;
291
+ if (
292
+ pointee_type.id () == ID_struct_tag || pointee_type.id () == ID_union_tag ||
293
+ pointee_type.id () == ID_array || pointee_type.id () == ID_struct ||
294
+ pointee_type.id () == ID_union)
295
+ return true ;
296
+ return false ;
297
+ }
298
+
272
299
exprt symbol_analyzert::get_pointer_value (
273
300
const exprt &expr,
274
301
const exprt &zero_expr,
@@ -293,9 +320,9 @@ exprt symbol_analyzert::get_pointer_value(
293
320
else
294
321
{
295
322
const exprt target_expr =
296
- (value. pointee . find ( " + " ) == std::string::npos )
297
- ? get_non_char_pointer_value (expr, memory_location , location)
298
- : get_pointer_to_member_value (expr, value , location);
323
+ points_to_member (value)
324
+ ? get_pointer_to_member_value (expr, value , location)
325
+ : get_non_char_pointer_value (expr, memory_location , location);
299
326
300
327
if (target_expr.id () == ID_nil)
301
328
{
@@ -395,6 +422,10 @@ exprt symbol_analyzert::get_expr_value(
395
422
396
423
return get_pointer_value (expr, zero_expr, location);
397
424
}
425
+ else if (type.id () == ID_union_tag)
426
+ {
427
+ return get_union_value (expr, zero_expr, location);
428
+ }
398
429
else
399
430
{
400
431
throw analysis_exceptiont (" unexpected expression:\n " + expr.pretty ());
@@ -436,6 +467,39 @@ exprt symbol_analyzert::get_struct_value(
436
467
return new_expr;
437
468
}
438
469
470
+ exprt symbol_analyzert::get_union_value (
471
+ const exprt &expr,
472
+ const exprt &zero_expr,
473
+ const source_locationt &location)
474
+ {
475
+ PRECONDITION (zero_expr.id () == ID_union);
476
+
477
+ PRECONDITION (expr.type ().id () == ID_union_tag);
478
+ PRECONDITION (expr.type () == zero_expr.type ());
479
+
480
+ exprt new_expr (zero_expr);
481
+
482
+ const union_tag_typet &union_tag_type = to_union_tag_type (expr.type ());
483
+ const union_typet union_type = ns.follow_tag (union_tag_type);
484
+
485
+ for (size_t i = 0 ; i < new_expr.operands ().size (); ++i)
486
+ {
487
+ const union_typet::componentt &component = union_type.components ()[i];
488
+
489
+ if (component.get_is_padding ())
490
+ {
491
+ continue ;
492
+ }
493
+
494
+ exprt &operand = new_expr.operands ()[i];
495
+ member_exprt member_expr (expr, component);
496
+
497
+ operand = get_expr_value (member_expr, operand, location);
498
+ }
499
+
500
+ return new_expr;
501
+ }
502
+
439
503
void symbol_analyzert::process_outstanding_assignments ()
440
504
{
441
505
for (const auto &pair : outstanding_assignments)
0 commit comments