diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index ad3a9f63d63c069d03fe90e47f16d5fb59dddc34..8317846aaa3afd18818c62b2c846b9d249e2b6e8 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -636,43 +636,30 @@ let process_pragmas_pack_align_field_attributes fi fattrs cattr = match !current_packing_pragma, align_pragma_for_struct fi.forig_name with | None, None -> check_aligned fattrs | Some n, apragma -> - begin - warn_incompatible_pragmas_attributes apragma (fattrs <> []); - match combine_aligned_attributes fattrs with - | None -> - (* No valid aligned attributes in this field. - – if the composite type has a packed attribute, nothing needs to be - done (the composite will have the "packed" attribute anyway); - – otherwise, align on min(n,sizeof(fi.ftyp)). - Drop existing "aligned" attributes, if there are invalid ones. *) - if Cil.hasAttribute "packed" cattr then (dropAttribute "aligned" fattrs) - else begin - let sizeof_type = - if Cil.isUnsizedArrayType fi.ftype - then - (* flexible array member: use size of pointer *) - Cil.bitsSizeOf (Machine.uintptr_type ()) - else - Cil.bytesSizeOf fi.ftype - in - let align = Integer.(min n (of_int sizeof_type)) in - Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true - "adding aligned(%a) attribute to field '%s.%s' due to packing pragma" - Integer.pretty align fi.fcomp.cname fi.fname; - addAttribute (Attr("aligned",[AInt align])) (dropAttribute "aligned" fattrs) - end - | Some local -> - (* There is an alignment attribute in this field. This may be smaller - than the field type alignment, so we get the maximum of both. - Then, we apply the pragma pack: the final alignment will be the - minimum between what we had and [n]. *) - let align = Integer.min n (Integer.max (Integer.of_int (Cil.bytesSizeOf fi.ftype)) local) in - Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true - "setting aligned(%a) attribute to field '%s.%s' due to packing pragma" - Integer.pretty align fi.fcomp.cname fi.fname; - addAttribute (Attr("aligned",[AInt align])) - (dropAttribute "aligned" fattrs) - end + warn_incompatible_pragmas_attributes apragma (fattrs <> []); + let field_align = combine_aligned_attributes fattrs in + (* If this field has no valid aligned attributes and the composite type + has a packed attribute, nothing needs to be done: the composite will + have the "packed" attribute anyway. *) + if field_align = None && Cil.hasAttribute "packed" cattr then + dropAttribute "aligned" fattrs + else + (* Otherwise, align on min(n, max(field alignment, type alignment)): + the field alignment attribute (if there is one) may be smaller than + its type alignment, so we get the maximum of both. Then, we apply + the pragma pack: the final alignment will be the minimum between what + we had and [n]. *) + let type_align = Integer.of_int (Cil.bytesAlignOf fi.ftype) in + let existing_align = + Option.fold field_align ~none:type_align ~some:(Integer.max type_align) + in + let new_align = Integer.min n existing_align in + Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true + "%s aligned(%a) attribute to field '%s.%s' due to packing pragma" + (if Option.is_none field_align then "adding" else "setting") + Integer.pretty new_align fi.fcomp.cname fi.fname; + let new_attr = Attr ("aligned", [AInt new_align]) in + addAttribute new_attr (dropAttribute "aligned" fattrs) | None, Some true -> dropAttribute "aligned" fattrs | None, Some false -> diff --git a/tests/misc/oracle/pragma-pack.1.res.oracle b/tests/misc/oracle/pragma-pack.1.res.oracle index 07e333489815dd5fba65f5eae1651ac0e17c1751..ee68d85c878caea4ef362845c0441af0f85f4eef 100644 --- a/tests/misc/oracle/pragma-pack.1.res.oracle +++ b/tests/misc/oracle/pragma-pack.1.res.oracle @@ -21,8 +21,8 @@ S_j ∈ {4} S_sizeof ∈ {16} PACK8_i ∈ {0} - PACK8_j ∈ {8} - PACK8_sizeof ∈ {24} + PACK8_j ∈ {4} + PACK8_sizeof ∈ {16} PACK1_i ∈ {0} PACK1_j ∈ {1} PACK1_sizeof ∈ {13}