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/dune b/tests/misc/dune
index 93eae8d4100a7dca3874f32ae2879a7bee91c003..1ac66020dfef15db60a3f578e47e78b01f746433 100644
--- a/tests/misc/dune
+++ b/tests/misc/dune
@@ -2,3 +2,9 @@
   (applies_to user_directories.unix.t)
   (enabled_if (and (= %{os_type} unix) (<> %{system} macos)))
 )
+
+(cram
+  (applies_to pragma-pack-gcc)
+  (enabled_if %{bin-available:gcc})
+  (deps pragma-pack.c pragma-pack-utils.h)
+)
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}
diff --git a/tests/misc/pragma-pack-gcc.t b/tests/misc/pragma-pack-gcc.t
new file mode 100644
index 0000000000000000000000000000000000000000..c68a6edf7ef6087b89bbeacd1f68f5382d3fb6d9
--- /dev/null
+++ b/tests/misc/pragma-pack-gcc.t
@@ -0,0 +1,11 @@
+Testing that the output produced by Eva and the execution of the binary
+compiled by GCC are identical, both on a 32-bit machdep and on a 64-bit one
+
+# Note: we cannot currently test this in Nix due to issues with multiStdenv
+#  $ frama-c pragma-pack.c -machdep gcc_x86_32 -eva -eva-msg-key=-summary | grep -A999 "eva:final-states" | grep -v "\[eva:final-states\]" | grep -v __retres > eva.res
+#  $ gcc -m32 pragma-pack.c -Wno-pragmas && ./a.out > gcc.res
+#  $ diff -B eva.res gcc.res # should be identical
+
+  $ frama-c pragma-pack.c -machdep gcc_x86_64 -eva -eva-msg-key=-summary | grep -A999 "eva:final-states" | grep -v "\[eva:final-states\]" | grep -v __retres > eva.res
+  $ gcc pragma-pack.c -Wno-pragmas && ./a.out > gcc.res
+  $ diff -B eva.res gcc.res # should be identical