From 6f9b3dfb1dd72e88fdc22776c8156c55e5988d0a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 3 Jul 2026 15:30:57 +0200 Subject: [PATCH] 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