diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 6a09fa82d14c464eee53c17d2aeb9a284880fff1..8c88a3af10b1598c786be81e67386363fd551c2a 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -317,7 +317,13 @@ struct
       let f = Context.get cframe in
       f.triggers <- tg :: f.triggers
 
-  let guards f = Lang.hypotheses f.gamma
+  let make_chunk_constraints f =
+    if not (Wp_parameters.RTE.get()) then []
+    else LabelMap.fold (fun _ s l -> M.is_well_formed s :: l) f.labels []
+
+  let guards f =
+    let constraints = in_frame f (fun () -> make_chunk_constraints f) () in
+    Lang.hypotheses f.gamma @ constraints
 
   (* -------------------------------------------------------------------------- *)
   (* --- Environments                                                       --- *)
@@ -438,6 +444,7 @@ struct
         let used = List.filter used_var sigv in
         let parp = List.map snd used in
         let sigp = List.map (fun (lv,_) -> Sig_value lv) used in
+        let domain = make_chunk_constraints frame @ domain in
         let (parm,sigm) =
           LabelMap.fold
             (fun label sigma acc ->
diff --git a/src/plugins/wp/MemEmpty.ml b/src/plugins/wp/MemEmpty.ml
index fc58ebd54acdc40d95ae067b1d845167f1311420..f10f6da7cef059c0cdeac2385976d338a97f4565 100644
--- a/src/plugins/wp/MemEmpty.ml
+++ b/src/plugins/wp/MemEmpty.ml
@@ -94,6 +94,7 @@ let loc_of_int _ _ = ()
 let int_of_loc _ () = e_zero
 
 let domain _obj _l = Sigma.Chunk.Set.empty
+let is_well_formed _s = p_true
 
 let source = "Empty Model"
 
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 18a27402314f57e34edb11a19541f494982bb18f..b717626bea998d91c4a13bdde52727de723ff4f2 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -700,6 +700,8 @@ let domain _obj = function
   | Lfld(_,_,_,ovl) -> Heap.of_overlay (map()) ovl
   | Larr(r,_,_,_,_,_) -> Heap.of_region (map()) r
 
+let is_well_formed _s = Lang.F.p_true
+
 let region_of_loc = function
   | (GarbledMix | Index _) as l -> error "Can not find region of %a" pretty l
   | Lref(r,_,_) | Lraw(r,_,_,_) | Lmem(r,_,_,_)
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index e1317a92d9400d83c597a36d0e216ab934cb86a1..fa4cb6ad40ad205e9b15848634576f785d9a935d 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -117,7 +117,7 @@ let pointer = Context.create "MemTyped.pointer"
 (* -------------------------------------------------------------------------- *)
 
 type chunk =
-  | M_int
+  | M_int of Ctypes.c_int
   | M_char
   | M_f32
   | M_f64
@@ -128,16 +128,20 @@ module Chunk =
 struct
   type t = chunk
   let self = "typed"
+  let int_rank = function
+    | CBool -> 0
+    | k -> Ctypes.i_bytes k * (if Ctypes.signed k then 2 else 1)
+
   let rank = function
-    | M_int -> 0
-    | M_char -> 1
-    | M_f32 -> 2
-    | M_f64 -> 3
-    | M_pointer -> 4
-    | T_alloc -> 5
+    | M_char -> -1
+    | M_int i -> int_rank i
+    | M_f32 -> 17
+    | M_f64 -> 18
+    | M_pointer -> 19
+    | T_alloc -> 20
   let hash = rank
   let name = function
-    | M_int -> "Mint"
+    | M_int _ -> "Mint"
     | M_char -> "Mchar"
     | M_f32 -> "Mf32"
     | M_f64 -> "Mf64"
@@ -147,13 +151,13 @@ struct
   let equal = (=)
   let pretty fmt c = Format.pp_print_string fmt (name c)
   let val_of_chunk = function
-    | M_int | M_char -> L.Int
+    | M_int _ | M_char -> L.Int
     | M_f32 -> Cfloat.tau_of_float Ctypes.Float32
     | M_f64 -> Cfloat.tau_of_float Ctypes.Float64
     | M_pointer -> t_addr
     | T_alloc -> L.Int
   let tau_of_chunk = function
-    | M_int | M_char -> L.Array(t_addr,L.Int)
+    | M_int _ | M_char -> L.Array(t_addr,L.Int)
     | M_pointer -> L.Array(t_addr,t_addr)
     | M_f32 -> L.Array(t_addr,Cfloat.tau_of_float Ctypes.Float32)
     | M_f64 -> L.Array(t_addr,Cfloat.tau_of_float Ctypes.Float64)
@@ -171,7 +175,7 @@ type loc = term (* of type addr *)
 (* --- Utilities on locations                                             --- *)
 (* -------------------------------------------------------------------------- *)
 
-let m_int i = if Ctypes.is_char i then M_char else M_int
+let m_int i = if Ctypes.is_char i then M_char else M_int i
 let m_float = function Float32 -> M_f32 | Float64 -> M_f64
 
 let rec footprint = function
@@ -871,6 +875,51 @@ let frames obj addr = function
       let basename = Chunk.basename_of_chunk m in
       MemMemory.frames ~addr ~offset ~sizeof ~basename tau
 
+(* -------------------------------------------------------------------------- *)
+(* --- Chunk element type                                                 --- *)
+(* -------------------------------------------------------------------------- *)
+
+module ChunkContent = WpContext.Generator(Chunk)
+    (struct
+      let name = "MemTyped.ChunkContent"
+      type key = Chunk.t
+      type data = lfun
+
+      let int_kind = function
+        | M_char -> Ctypes.c_char ()
+        | M_int k -> k
+        | _ -> failwith "MemTyped asked constraint for non int type"
+
+      let generate c =
+        let k = int_kind c in
+        let p = Lang.freshvar ~basename:"m" (Chunk.tau_of_chunk c) in
+        let m = e_var p in
+        let name = Format.asprintf "is_%a_chunk" Ctypes.pp_int k in
+        let lfun = Lang.generated_p name in
+        let l = Lang.freshvar ~basename:"l" (Lang.t_addr()) in
+        let is_int = Cint.range k in
+        let def = p_forall [l] (is_int (F.e_get m (e_var l))) in
+        Definitions.define_symbol {
+          d_lfun = lfun ; d_types = 0 ;
+          d_params = [p] ;
+          d_definition = Predicate(Def, def) ;
+          d_cluster = cluster ~id:"Chunk" ~title:"Chunk type constraint" () ;
+        } ;
+        lfun
+
+      let compile = Lang.local generate
+    end)
+
+let is_chunk sigma = function
+  | M_int _ | M_char as m ->
+      F.p_call (ChunkContent.get m) [ Sigma.value sigma m ]
+  | _ ->
+      p_true
+
+let is_well_formed sigma =
+  let open Sigma in
+  p_conj (Chunk.Set.fold (fun c l -> is_chunk sigma c :: l) (domain sigma) [])
+
 (* -------------------------------------------------------------------------- *)
 (* --- Loader                                                             --- *)
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index fd09f824c2c909084efb61b68f5abcd6ab51956e..e07a9ad259adcc5d0bf587c98ba2fc57ddb48caf 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -1267,6 +1267,9 @@ struct
           (fun m s -> Heap.Set.add (Mem m) s)
           (M.domain obj (mloc_of_loc l)) Heap.Set.empty
 
+  let is_well_formed sigma =
+    M.is_well_formed sigma.mem
+
   (* -------------------------------------------------------------------------- *)
 
 end
diff --git a/src/plugins/wp/MemZeroAlias.ml b/src/plugins/wp/MemZeroAlias.ml
index 19f271238f13ffc3b9049c6f4b2695e8488b2f78..c734daed7a612645c844dd3351f711eb9328bfcf 100644
--- a/src/plugins/wp/MemZeroAlias.ml
+++ b/src/plugins/wp/MemZeroAlias.ml
@@ -183,6 +183,8 @@ let domain _obj l =
   try Heap.Set.singleton (fst (access l))
   with _ -> Heap.Set.empty
 
+let is_well_formed _s = p_true
+
 let value sigma l =
   let m,ks = access l in
   let x = Sigma.get sigma m in
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 72d1972ac59d46b817f11284ffa445c843d75af7..6f8f2636caefcc70f64d661a1c46e85e6f56c81a 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -412,6 +412,10 @@ sig
       the given C-type. It is safe to retun an over-approximation of the
       chunks involved. *)
 
+  val is_well_formed : sigma -> pred
+  (** Provides the constraint corresponding to the kind of data stored by all
+      chunks in sigma. *)
+
   val load : sigma -> c_object -> loc -> loc value
   (** Return the value of the object of the given type at the given location in
       the given memory state. *)
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 6108632979a7df27f72538793ef5881df0f49d37..b8389519cc2b552a62d28100f2ae7c1b8b7ecab1 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -207,11 +207,15 @@ struct
   let intersect_vc vc p =
     Vars.intersect (F.varsp p) vc.vars || Conditions.intersect p vc.hyps
 
-  let state_vc ?descr ?stmt state vc =
+  let state_vc ?descr ?stmt sigma state vc =
     let path = match stmt with
       | None -> vc.path
       | Some s -> S.add s vc.path in
-    let hyps = Conditions.state ?stmt ?descr state vc.hyps in
+    let hyps =
+      if not (Wp_parameters.RTE.get()) then vc.hyps
+      else Conditions.domain [M.is_well_formed sigma] vc.hyps
+    in
+    let hyps = Conditions.state ?stmt ?descr state hyps in
     { vc with path ; hyps }
 
   let assume_vc ?descr ?hpid ?stmt ?warn
@@ -640,7 +644,7 @@ struct
         | Some { labels = lbl::_ } ->
             Some (Pretty_utils.to_string Printer.pp_label lbl) in
       let state = Mstate.state state sigma in
-      gmap (state_vc ?descr ?stmt state) vcs
+      gmap (state_vc ?descr ?stmt sigma state) vcs
     with Not_found -> vcs
 
   let label wenv stmt label wp =
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
index e519f55833a656ae85bc1acda6610c6ee0f85398..85d318865a1934c7bb5c8f657a5ea7317cb64852 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
@@ -71,19 +71,10 @@ Let a = global(G_tr_35).
 Let a_1 = shift___anonstruct_Point_1(a, 2).
 Let a_2 = shift___anonstruct_Point_1(a, 1).
 Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = shiftfield_F4_bytes(global(G_buint_41)).
 Let m = Array1_S1(a, 3, Mint_0).
 Assume {
   Type: IsArray1S1(m) /\ IsArray1S1(Array1_S1(a_3, 3, Mint_0)).
   (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 0)] = 1.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 1)] = 2.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 2)] = 4.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 3)] = 8.
-  (* Initializer *)
   Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
   (* Initializer *)
   Init: Mint_0[shiftfield_F1_y(a_3)] = 11.
@@ -105,19 +96,10 @@ Let a = global(G_tr_35).
 Let a_1 = shift___anonstruct_Point_1(a, 2).
 Let a_2 = shift___anonstruct_Point_1(a, 1).
 Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = shiftfield_F4_bytes(global(G_buint_41)).
 Let m = Array1_S1(a, 3, Mint_0).
 Assume {
   Type: IsArray1S1(m) /\ IsArray1S1(Array1_S1(a_3, 3, Mint_0)).
   (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 0)] = 1.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 1)] = 2.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 2)] = 4.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 3)] = 8.
-  (* Initializer *)
   Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
   (* Initializer *)
   Init: Mint_0[shiftfield_F1_y(a_3)] = 11.
@@ -139,19 +121,10 @@ Let a = global(G_tr_35).
 Let a_1 = shift___anonstruct_Point_1(a, 2).
 Let a_2 = shift___anonstruct_Point_1(a, 1).
 Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = shiftfield_F4_bytes(global(G_buint_41)).
 Let m = Array1_S1(a_3, 3, Mint_0).
 Assume {
   Type: IsArray1S1(Array1_S1(a, 3, Mint_0)) /\ IsArray1S1(m).
   (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 0)] = 1.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 1)] = 2.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 2)] = 4.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_4, 3)] = 8.
-  (* Initializer *)
   Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
   (* Initializer *)
   Init: Mint_0[shiftfield_F1_y(a_3)] = 11.
@@ -220,37 +193,21 @@ Goal Pre-condition 'qed_ok' in 'main':
 tests/wp_acsl/logic.i:55: warning from wp:
  - Warning: Hide sub-term definition
    Reason: Logic cast to struct (Buint) from (unsigned int) not implemented yet
-Let a = global(G_tr_35).
-Let a_1 = shift___anonstruct_Point_1(a, 2).
-Let a_2 = shift___anonstruct_Point_1(a, 1).
-Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = global(G_buint_41).
-Let a_5 = shiftfield_F4_bytes(a_4).
-Let a_6 = Load_S4(a_4, Mint_0).
+Let a = global(G_buint_41).
+Let a_1 = shiftfield_F4_bytes(a).
+Let a_2 = Load_S4(a, Mint_0).
 Assume {
-  Type: IsS4(a_6).
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_5, 0)] = 1.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_5, 1)] = 2.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_5, 2)] = 4.
-  (* Initializer *)
-  Init: Mint_0[shift_uint8(a_5, 3)] = 8.
-  (* Initializer *)
-  Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
+  Type: IsS4(a_2).
   (* Initializer *)
-  Init: Mint_0[shiftfield_F1_y(a_3)] = 11.
+  Init: Mint_0[shift_uint8(a_1, 0)] = 1.
   (* Initializer *)
-  Init: Mint_0[shiftfield_F1_x(a_2)] = 20.
+  Init: Mint_0[shift_uint8(a_1, 1)] = 2.
   (* Initializer *)
-  Init: Mint_0[shiftfield_F1_y(a_2)] = 21.
+  Init: Mint_0[shift_uint8(a_1, 2)] = 4.
   (* Initializer *)
-  Init: Mint_0[shiftfield_F1_x(a_1)] = 30.
-  (* Initializer *)
-  Init: Mint_0[shiftfield_F1_y(a_1)] = 31.
+  Init: Mint_0[shift_uint8(a_1, 3)] = 8.
 }
-Prove: EqS4(a_6, w).
+Prove: EqS4(a_2, w).
 
 ------------------------------------------------------------