From 6f9b3dfb1dd72e88fdc22776c8156c55e5988d0a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 3 Jul 2026 15:30:57 +0200 Subject: [PATCH 1/2] Reject `aligned` attribute on bit fields in struct types Just like we already reject `_Alignas(N)` on bit fields. Alignment on bit fields was already ignored by the verified part of CompCert. --- cparser/Cutil.ml | 2 ++ cparser/Elab.ml | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 0ef96ddd1..9c11dcec5 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -609,6 +609,8 @@ let sizeof_layout_struct env members ma = (record_field m.fld_name pos :: accu) rem | Some width -> + (* bit fields must be naturally aligned *) + assert (alignas_attribute (attributes_of_type env m.fld_typ) = 0); (* curr = beginning of storage unit, in bits next = one past end of storage unit, in bits *) let curr = pos / (a * 8) * (a * 8) in diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 7bbb43199..dc2a3c62c 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1086,7 +1086,7 @@ and elab_field_group env = function error loc "the type of bit-field '%a' must be an integer type no bigger than 'int'" pp_field id; None,env - end else if has_std_alignas env' ty then begin + end else if alignas_attribute (attributes_of_type env' ty) > 0 then begin error loc "alignment specified for bit-field '%a'" pp_field id; None, env end else begin From d3e6f6360ed81e1d30cae138f85adad2971025d5 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 6 Jul 2026 14:31:44 +0200 Subject: [PATCH 2/2] Do not change alignment for packed bit-fields Bit-fields are not allowed in packed structs and reducing the alignment leads is also not allowed, so we report the error and do not change the field. --- cparser/PackedStructs.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index f3a457856..3ba0ab056 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -74,11 +74,13 @@ let transf_field_decl mfa swapped loc env struct_id f = end; (* Reduce alignment if requested *) if mfa = 0 then f else begin - if f.fld_bitfield <> None then + if f.fld_bitfield <> None then begin error loc "bit fields in packed structs are not supported"; - let al = safe_alignof loc env f.fld_typ in - { f with fld_typ = - change_attributes_type env (set_alignas_attr (min mfa al)) f.fld_typ } + f + end else + let al = safe_alignof loc env f.fld_typ in + { f with fld_typ = + change_attributes_type env (set_alignas_attr (min mfa al)) f.fld_typ } end (* Rewriting struct declarations *)