diff --git a/src/plugins/builtin/stdlib/basic_alloc.ml b/src/plugins/builtin/stdlib/basic_alloc.ml
index 2d0252c539d70a9e8be4efe738e08007844d939e..98de973cb61e1dc8094809a24928f3cbdd4c77e2 100644
--- a/src/plugins/builtin/stdlib/basic_alloc.ml
+++ b/src/plugins/builtin/stdlib/basic_alloc.ml
@@ -21,11 +21,33 @@
 (**************************************************************************)
 
 open Logic_const
+open Basic_blocks
 open Cil_types
+open Extlib
+
+let valid_size ?loc typ size =
+  let p = match typ with
+    | TComp (ci, _, _) when Cil.has_flexible_array_member typ ->
+      let elem = match (last ci.cfields).ftype with
+        | TArray(t, _ , _, _) -> tinteger ?loc (Cil.bytesSizeOf t)
+        | _ -> assert false
+      in
+      let base = tinteger ?loc (Cil.bytesSizeOf typ) in
+      let flex = tminus ?loc size base in
+      let flex_mod = term ?loc (TBinOp(Mod, flex, elem)) Linteger in
+      let flex_at_least_zero = prel ?loc (Rle, Cil.lzero (), flex) in
+      let aligned_flex = prel ?loc (Req, Cil.lzero (), flex_mod) in
+      pand ?loc (flex_at_least_zero, aligned_flex)
+    | _ ->
+      let elem = tinteger ?loc (Cil.bytesSizeOf typ) in
+      let modulo = term ?loc (TBinOp(Mod, size, elem)) Linteger in
+      prel(Req, Cil.lzero (), modulo)
+  in
+  new_predicate { p with pred_name = ["correct_size"] }
 
 let pis_allocable ?loc size =
   let is_allocable = Logic_env.find_all_logic_functions "is_allocable" in
-  let is_allocable = Extlib.as_singleton is_allocable in
+  let is_allocable = as_singleton is_allocable in
   papp ?loc (is_allocable, [here_label], [size])
 
 let is_allocable ?loc size =
diff --git a/src/plugins/builtin/stdlib/basic_alloc.mli b/src/plugins/builtin/stdlib/basic_alloc.mli
index 0ff9e7864da07c8ad5d66ef3564d396a91d54441..611b4c12634aeab13776fabb61309e8701c5aad4 100644
--- a/src/plugins/builtin/stdlib/basic_alloc.mli
+++ b/src/plugins/builtin/stdlib/basic_alloc.mli
@@ -22,6 +22,8 @@
 
 open Cil_types
 
+val valid_size: ?loc:location -> typ -> term -> identified_predicate
+
 val is_allocable: ?loc:location -> term -> identified_predicate
 val isnt_allocable: ?loc:location -> term -> identified_predicate
 
diff --git a/src/plugins/builtin/stdlib/calloc.ml b/src/plugins/builtin/stdlib/calloc.ml
index 996940ac15512471efe967b60a61df5928164b99..a716c5cdbd4ea97120e92c91e5c5e9e1afe7755b 100644
--- a/src/plugins/builtin/stdlib/calloc.ml
+++ b/src/plugins/builtin/stdlib/calloc.ml
@@ -41,17 +41,21 @@ let pset_len_to_zero ?loc ptr_type len =
   let p = punfold_all_elems_pred ?loc result len eq_value in
   new_predicate { p with pred_name = [ "zero_initialization" ] }
 
+let generate_requires ?loc alloc_typ num size =
+  let only_one = if Cil.has_flexible_array_member alloc_typ then
+    let p = prel ?loc (Req, num, Cil.lone ?loc ()) in
+    Some (new_predicate { p with pred_name = ["only_one"] })
+  else
+    None
+  in
+  [ valid_size ?loc alloc_typ size ] @ (Extlib.list_of_opt only_one)
+
 let pinitialized_len ?loc ptr_type len =
   let result = tresult ?loc ptr_type in
   let initialized ?loc t = pinitialized ?loc (here_label, t) in
   let p = punfold_all_elems_pred ?loc result len initialized in
   new_predicate { p with pred_name = [ "initialization" ] }
 
-let generate_requires loc ptr_type len =
-  [ new_predicate
-      { (pcorrect_len_bytes ~loc ptr_type len)
-        with pred_name = ["aligned_end"] } ]
-
 let generate_global_assigns loc ptr_type num size =
   let assigns_result = assigns_result ~loc ptr_type [ num ; size ] in
   let assigns_heap = assigns_heap [ num ; size ] in
@@ -84,7 +88,7 @@ let generate_spec alloc_typ { svar = vi } loc =
   in
   let num = tlogic_coerce ~loc (cvar_to_tvar cnum) Linteger in
   let size = tlogic_coerce ~loc (cvar_to_tvar csize) Linteger in
-  let requires = generate_requires loc (Ctype (ptr_of alloc_typ)) size in
+  let requires = generate_requires ~loc alloc_typ num size in
   let assigns = generate_global_assigns loc (ptr_of alloc_typ) num size in
   let alloc = allocates_result ~loc (ptr_of alloc_typ) in
   make_funspec [
diff --git a/src/plugins/builtin/stdlib/malloc.ml b/src/plugins/builtin/stdlib/malloc.ml
index 212f7b4a102f24d5c0817d9b092a1bbfa6085466..a696a6f6af1a04a872b8a0e6c2257398caf02809 100644
--- a/src/plugins/builtin/stdlib/malloc.ml
+++ b/src/plugins/builtin/stdlib/malloc.ml
@@ -27,11 +27,6 @@ open Logic_const
 
 let function_name = "malloc"
 
-let generate_requires loc ptr_type size =
-  [ new_predicate
-      { (pcorrect_len_bytes ~loc ptr_type size)
-        with pred_name = ["aligned_end"] } ]
-
 let generate_global_assigns loc ptr_type size =
   let assigns_result = assigns_result ~loc ptr_type [ size ] in
   let assigns_heap = assigns_heap [ size ] in
@@ -57,7 +52,7 @@ let generate_spec alloc_typ { svar = vi } loc =
     | _ -> assert false
   in
   let size = tlogic_coerce ~loc (cvar_to_tvar csize) Linteger in
-  let requires = generate_requires loc (Ctype (ptr_of alloc_typ)) size in
+  let requires = [ valid_size ~loc alloc_typ size ] in
   let assigns = generate_global_assigns loc (ptr_of alloc_typ) size in
   let alloc = allocates_result ~loc (ptr_of alloc_typ) in
   make_funspec [