@@ -206,10 +206,19 @@ exprt symbol_analyzert::get_pointer_to_member_value(
206206 PRECONDITION (!pointer_value.pointee .empty ());
207207
208208 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+ }
213222
214223 const symbolt *struct_symbol = symbol_table.lookup (struct_name);
215224 DATA_INVARIANT (struct_symbol != nullptr , " unknown struct" );
@@ -269,6 +278,24 @@ exprt symbol_analyzert::get_non_char_pointer_value(
269278 }
270279}
271280
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+
272299exprt symbol_analyzert::get_pointer_value (
273300 const exprt &expr,
274301 const exprt &zero_expr,
@@ -293,9 +320,9 @@ exprt symbol_analyzert::get_pointer_value(
293320 else
294321 {
295322 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);
299326
300327 if (target_expr.id () == ID_nil)
301328 {
@@ -395,6 +422,10 @@ exprt symbol_analyzert::get_expr_value(
395422
396423 return get_pointer_value (expr, zero_expr, location);
397424 }
425+ else if (type.id () == ID_union_tag)
426+ {
427+ return get_union_value (expr, zero_expr, location);
428+ }
398429 else
399430 {
400431 throw analysis_exceptiont (" unexpected expression:\n " + expr.pretty ());
@@ -436,6 +467,39 @@ exprt symbol_analyzert::get_struct_value(
436467 return new_expr;
437468}
438469
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+
439503void symbol_analyzert::process_outstanding_assignments ()
440504{
441505 for (const auto &pair : outstanding_assignments)
0 commit comments