diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 0bfde596c3a5a58f79426bb00d5e24df90604f56..9f5bc00b9ef58384a6da6bc0054704977386b86d 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -349,13 +349,15 @@ let is_aligned_by b alignment =
   if Int.is_zero alignment
   then false
   else
-    match b with
-    | Var (v,_) | Allocated(v,_,_) ->
-      Int.is_zero (Int.e_rem (Int.of_int (Cil.bytesAlignOf v.vtype)) alignment)
-    | CLogic_Var (_, ty, _) ->
-      Int.is_zero (Int.e_rem (Int.of_int (Cil.bytesAlignOf ty)) alignment)
-    | Null -> true
-    | String _ -> Int.is_one alignment
+    try
+      match b with
+      | Var (v,_) | Allocated(v,_,_) ->
+        Int.is_zero (Int.e_rem (Int.of_int (Cil.bytesAlignOf v.vtype)) alignment)
+      | CLogic_Var (_, ty, _) ->
+        Int.is_zero (Int.e_rem (Int.of_int (Cil.bytesAlignOf ty)) alignment)
+      | Null -> true
+      | String _ -> Int.is_one alignment
+    with Cil.SizeOfError _ -> false
 
 let is_any_formal_or_local v =
   match v with
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 81f75901401bc71cf31618912dfa25307599e761..203845899acaf1d53dd33ff0b842fd4c93081eb5 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -4545,7 +4545,10 @@ and constFold (machdep: bool) (e: exp) : exp =
   | SizeOfStr s when machdep ->
     kinteger ~loc theMachine.kindOfSizeOf (1 + String.length s)
   | AlignOf t when machdep ->
-    kinteger ~loc theMachine.kindOfSizeOf (bytesAlignOf t)
+    begin
+      try kinteger ~loc theMachine.kindOfSizeOf (bytesAlignOf t)
+      with SizeOfError _ -> e
+    end
   | AlignOfE e when machdep -> begin
       (* The alignment of an expression is not always the alignment of its
        * type. I know that for strings this is not true *)
@@ -5223,7 +5226,11 @@ let rec constFoldTermNodeAtTop = function
     (try integer_lconstant (bytesSizeOf typ)
      with SizeOfError _ -> t)
   | TSizeOfStr str -> integer_lconstant (String.length str + 1)
-  | TAlignOf typ -> integer_lconstant (bytesAlignOf typ)
+  | TAlignOf typ as t ->
+    begin
+      try integer_lconstant (bytesAlignOf typ)
+      with SizeOfError _ -> t
+    end
   | TSizeOfE { term_type= Ctype typ } -> constFoldTermNodeAtTop (TSizeOf typ)
   | TAlignOfE { term_type= Ctype typ }
     -> 	constFoldTermNodeAtTop (TAlignOf typ)
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 02f54e2f020e25934ad25cddffb08a467da39b65..2613a70e4cf8cc0f4e924d611b0c57aa3f0ff9f6 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2183,7 +2183,8 @@ val sizeOf: loc:location -> typ -> exp
 
 (** The minimum alignment (in bytes) for a type. This function is
  * architecture dependent, so you should only call this after you call
- * {!Cil.initCIL}. *)
+ * {!Cil.initCIL}.
+ * Raises {!SizeOfError} when it cannot compute the alignment. *)
 val bytesAlignOf: typ -> int
 
 (** [intOfAttrparam a] tries to const-fold [a] into a numeric value.
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index ab451611348a7ad2d828eb43eeac5f8de28ae100..4668403ccdd3a40572022f3df66406c9e02ca0e0 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -406,7 +406,9 @@ let infer_sizeof ty =
   try singleton_of_int (Cil.bytesSizeOf ty)
   with Cil.SizeOfError _ -> interv_of_typ Cil.theMachine.Cil.typeOfSizeOf
 
-let infer_alignof ty = singleton_of_int (Cil.bytesAlignOf ty)
+let infer_alignof ty =
+  try singleton_of_int (Cil.bytesAlignOf ty)
+  with Cil.SizeOfError _ -> interv_of_typ Cil.theMachine.Cil.typeOfSizeOf
 
 let rec infer t =
   let get_cty t = match t.term_type with Ctype ty -> ty | _ -> assert false in