diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 82e08770fa7d4e69435957afd2621665c4fdb9eb..cffc3e6654fad1bb2fd58686416c6da4e46ed957 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -4085,7 +4085,7 @@ let rec bytesAlignOf t =
       else
         raise (SizeOfError ("Undefined sizeof(void).", t))
   in
-  process_aligned_attribute ~may_reduce:false
+  process_aligned_attribute ~may_reduce:true
     (fun fmt -> !pp_typ_ref fmt t)
     (typeAttrs t) alignOfType
 
@@ -4165,8 +4165,11 @@ and process_aligned_attribute (pp:Format.formatter->unit) ~may_reduce attrs defa
      (e.g. a "packed" attribute is present).
      According to GCC's doc
      (https://gcc.gnu.org/onlinedocs/gcc/Common-Type-Attributes.html):
-     "The aligned attribute can only increase alignment.
-      Alignment can be decreased by specifying the packed attribute." *)
+     "When used on a struct, or struct member, the aligned attribute can only
+     increase the alignment; in order to decrease it, the packed attribute must
+     be specified as well. When used as part of a typedef, the aligned attribute
+     can both increase and decrease alignment, and specifying the packed
+     attribute generates a warning." *)
   match filterAttributes "aligned" attrs with
   | [] ->
     (* no __aligned__ attribute, so get the default alignment *)
diff --git a/tests/value/attribute-aligned.c b/tests/value/attribute-aligned.c
index 2aede3793e86b686a3dd9cf1bca8c0c3e92002e8..c7c04614746f37c5374f6d550caa2c114f178ed3 100644
--- a/tests/value/attribute-aligned.c
+++ b/tests/value/attribute-aligned.c
@@ -90,6 +90,18 @@ static void tt(void) {
   // frama-c :   8  : |a---b---| : b of size 1 instead of 0
 }
 
+//--------------------------------------------------------------------
+typedef float float_aligned16 __attribute__((aligned(16))); // increase
+typedef double double_aligned1 __attribute__((aligned(1))); // reduce
+
+static void typedef_with_aligned(void) {
+  int a;
+  a = __alignof__(float_aligned16);
+  //@ check a == 16;
+  a = __alignof__(double_aligned1);
+  //@ check a == 1;
+}
+
 //--------------------------------------------------------------------
 
 int main(void)
@@ -101,5 +113,6 @@ int main(void)
   rt();
   st();
   tt();
+  typedef_with_aligned();
   return 0;
 }
diff --git a/tests/value/oracle/attribute-aligned.res.oracle b/tests/value/oracle/attribute-aligned.res.oracle
index 74ec1f2bbed00d64b779385716e3b47b6701a179..0ce8c8d3bc4d74b394114b03d10e9c1f9433f66e 100644
--- a/tests/value/oracle/attribute-aligned.res.oracle
+++ b/tests/value/oracle/attribute-aligned.res.oracle
@@ -7,33 +7,39 @@
   A ∈ {0}
   B ∈ {0}
 [eva] computing for function ct <- main.
-  Called from attribute-aligned.c:97.
+  Called from attribute-aligned.c:109.
 [eva] Recording results for ct
 [eva] Done for function ct
 [eva] computing for function dt <- main.
-  Called from attribute-aligned.c:98.
+  Called from attribute-aligned.c:110.
 [eva] Recording results for dt
 [eva] Done for function dt
 [eva] computing for function pt <- main.
-  Called from attribute-aligned.c:99.
+  Called from attribute-aligned.c:111.
 [eva] Recording results for pt
 [eva] Done for function pt
 [eva] computing for function qt <- main.
-  Called from attribute-aligned.c:100.
+  Called from attribute-aligned.c:112.
 [eva] Recording results for qt
 [eva] Done for function qt
 [eva] computing for function rt <- main.
-  Called from attribute-aligned.c:101.
+  Called from attribute-aligned.c:113.
 [eva] Recording results for rt
 [eva] Done for function rt
 [eva] computing for function st <- main.
-  Called from attribute-aligned.c:102.
+  Called from attribute-aligned.c:114.
 [eva] Recording results for st
 [eva] Done for function st
 [eva] computing for function tt <- main.
-  Called from attribute-aligned.c:103.
+  Called from attribute-aligned.c:115.
 [eva] Recording results for tt
 [eva] Done for function tt
+[eva] computing for function typedef_with_aligned <- main.
+  Called from attribute-aligned.c:116.
+[eva] attribute-aligned.c:100: check got status valid.
+[eva] attribute-aligned.c:102: check got status valid.
+[eva] Recording results for typedef_with_aligned
+[eva] Done for function typedef_with_aligned
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -62,6 +68,8 @@
   S ∈ {4}
   A ∈ {0}
   B ∈ {4}
+[eva:final-states] Values at end of function typedef_with_aligned:
+  a ∈ {1}
 [eva:final-states] Values at end of function main:
   S ∈ {4}
   A ∈ {0}
@@ -81,6 +89,8 @@
 [from] Done for function st
 [from] Computing for function tt
 [from] Done for function tt
+[from] Computing for function typedef_with_aligned
+[from] Done for function typedef_with_aligned
 [from] Computing for function main
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
@@ -110,6 +120,8 @@
   S FROM \nothing
   A FROM \nothing
   B FROM \nothing
+[from] Function typedef_with_aligned:
+  NO EFFECTS
 [from] Function main:
   S FROM \nothing
   A FROM \nothing
@@ -144,6 +156,10 @@
     S; A; B
 [inout] Inputs for function tt:
     \nothing
+[inout] Out (internal) for function typedef_with_aligned:
+    a
+[inout] Inputs for function typedef_with_aligned:
+    \nothing
 [inout] Out (internal) for function main:
     S; A; B; __retres
 [inout] Inputs for function main: