diff --git a/src/plugins/wp/MemAddr.ml b/src/plugins/wp/MemAddr.ml
new file mode 100644
index 0000000000000000000000000000000000000000..325ee2b04bfa2b52c0b896a7adaaf18b583c64cd
--- /dev/null
+++ b/src/plugins/wp/MemAddr.ml
@@ -0,0 +1,417 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of WP plug-in of Frama-C.                           *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2023                                               *)
+(*    CEA (Commissariat a l'energie atomique et aux energies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Lang.F
+
+(* -------------------------------------------------------------------------- *)
+(* --- Symbols registration                                               --- *)
+(* -------------------------------------------------------------------------- *)
+
+let library = "memaddr"
+
+(* Warning: DO NOT register map types using this constructor: it hides types
+   needed by ProverWhy3 for typing terms of the form x[i].
+*)
+
+let t_addr = Qed.Logic.Data(Lang.datatype ~library "addr",[])
+let t_table = Qed.Logic.Data(Lang.datatype ~library "table",[])
+
+let f_base   = Lang.extern_f ~library ~result:Qed.Logic.Int
+    ~link:(Qed.Engine.F_subst ("base", "%1.base")) "base"
+
+let f_offset = Lang.extern_f ~library ~result:Qed.Logic.Int
+    ~link:(Qed.Engine.F_subst ("offset", "%1.offset")) "offset"
+
+let f_shift  = Lang.extern_f ~library ~result:t_addr "shift"
+let f_global = Lang.extern_f ~library ~result:t_addr ~category:Qed.Logic.Injection "global"
+let f_null   = Lang.extern_f ~library ~result:t_addr "null"
+
+let p_addr_lt = Lang.extern_p ~library ~bool:"addr_lt_bool" ~prop:"addr_lt" ()
+let p_addr_le = Lang.extern_p ~library ~bool:"addr_le_bool" ~prop:"addr_le" ()
+
+let f_addr_of_int = Lang.extern_f
+    ~category:Qed.Logic.Injection
+    ~library ~result:t_addr "addr_of_int"
+
+let f_int_of_addr = Lang.extern_f
+    ~category:Qed.Logic.Injection
+    ~library ~result:Qed.Logic.Int "int_of_addr"
+
+
+let f_table_of_base = Lang.extern_f ~library
+    ~category:Qed.Logic.Function ~result:t_table "table_of_base"
+
+let f_table_to_offset = Lang.extern_f ~library
+    ~category:Qed.Logic.Injection ~result:Qed.Logic.Int "table_to_offset"
+
+let p_valid_rd = Lang.extern_fp ~library "valid_rd"
+let p_valid_rw = Lang.extern_fp ~library "valid_rw"
+let p_valid_obj = Lang.extern_fp ~library "valid_obj"
+let p_invalid = Lang.extern_fp ~library "invalid"
+let p_separated = Lang.extern_fp ~library "separated"
+let p_included = Lang.extern_fp ~library "included"
+
+(* base -> region *)
+let f_region = Lang.extern_f ~coloring:true ~library ~result:Qed.Logic.Int "region"
+(* allocation-table -> prop *)
+let p_linked = Lang.extern_fp ~coloring:true ~library "linked"
+
+(* -------------------------------------------------------------------------- *)
+(* --- API                                                                --- *)
+(* -------------------------------------------------------------------------- *)
+
+let base addr = e_fun f_base [ addr ]
+let offset addr = e_fun f_offset [ addr ]
+let null = constant (e_fun f_null [])
+let global base = e_fun f_global [ base ]
+let shift addr offset = e_fun f_shift [ addr ; offset ]
+let mk_addr base offset = shift (global base) offset
+
+let addr_lt addr1 addr2 = p_call p_addr_lt [ addr1 ; addr2 ]
+let addr_le addr1 addr2 = p_call p_addr_le [ addr1 ; addr2 ]
+
+let addr_of_int i = e_fun f_addr_of_int [ i ]
+let int_of_addr addr = e_fun f_int_of_addr [ addr ]
+
+let base_offset base offset =
+  let offset_index = e_fun f_table_of_base [base] in
+  e_fun f_table_to_offset [offset_index ; offset]
+(** Returns the offset in {i bytes} from the {i logic} offset
+    (which is a memory cell index, actually) *)
+
+let valid_rd alloc addr size = p_call p_valid_rd [ alloc ; addr ; size ]
+let valid_rw alloc addr size = p_call p_valid_rw [ alloc ; addr ; size ]
+let valid_obj alloc addr size = p_call p_valid_obj [ alloc ; addr ; size ]
+let invalid alloc addr size = p_call p_invalid [ alloc ; addr ; size ]
+
+let region base = e_fun f_region [ base ]
+let linked memory = p_call p_linked [ memory ]
+
+(* -------------------------------------------------------------------------- *)
+(* --- Qed Simplifiers                                                    --- *)
+(* -------------------------------------------------------------------------- *)
+
+(*
+    Pointer arithmetic for structure access and array access could be
+    defined directly using the record [{ base = p.base; offset = p.offset
+    + c*i + c' }]. However that gives very bad triggers for the memory
+    model axiomatization, so `shift p (c*i+c')` was used instead. It is
+    not sufficient for user axiomatisation because memory access in
+    axioms require trigger with arithmetic operators which is badly
+    handled by provers. So for each c and c', ie for each kind of
+    structure access and array access a specific function is used
+    `shift_xxx`.
+
+    Moreover no simplification of `shift_xxx` is done for keeping the
+    same terms in axioms and the goal. `base` and `offset` function
+    simplify all the `shift_xxx` because it seems they don't appear
+    often in axioms and they are useful for simplifying `separated`,
+    `assigns` and pointer comparisons in goals.
+
+    To sum up memory access should match, but not `\base`, `\offset`,
+    `\separated`, ...
+*)
+
+type addr_builtin = {
+  base: term list -> term ;
+  offset: term list -> term ;
+}
+
+module ADDR_BUILTIN = WpContext.Static
+    (struct
+      type key = Lang.lfun
+      type data = addr_builtin
+      let name = "MemMemory.ADDR_BUILTIN"
+      include Lang.Fun
+    end)
+
+let phi_base l =
+  match repr l with
+  | Fun(f,[p;_]) when f==f_shift -> base p
+  | Fun(f,[b]) when f==f_global -> b
+  | Fun(f,[]) when f==f_null -> e_zero
+  | Fun(f,args) -> (ADDR_BUILTIN.find f).base args
+  | _ -> raise Not_found
+
+let phi_offset l = match repr l with
+  | Fun(f,[p;k]) when f==f_shift -> e_add (offset p) k
+  | Fun(f,_) when f==f_global || f==f_null -> e_zero
+  | Fun(f,args) -> (ADDR_BUILTIN.find f).offset args
+  | _ -> raise Not_found
+
+let phi_shift f p i =
+  match repr p with
+  | Fun(g,[q;j]) when f == g -> e_fun f [q;e_add i j]
+  | _ -> raise Not_found
+
+let eq_shift a b =
+  let p = base a in
+  let q = base b in
+  let i = offset a in
+  let j = offset b in
+  if i==j then p_equal p q else
+    match is_equal p q with
+    | No -> p_false
+    | Yes -> p_equal i j
+    | Maybe -> raise Not_found
+
+let eq_shift_gen phi a b =
+  try phi a b with Not_found -> eq_shift a b
+
+let nop _ = raise Not_found
+
+let register ?(base=nop) ?(offset=nop) ?equal ?(linear=false) lfun =
+  begin
+    if base != nop || offset != nop then
+      ADDR_BUILTIN.define lfun { base ; offset } ;
+    if linear then
+      set_builtin_2 lfun (phi_shift lfun) ;
+    let phi_equal = match equal with
+      | None -> eq_shift
+      | Some phi -> eq_shift_gen phi
+    in
+    set_builtin_eqp lfun phi_equal ;
+  end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Simplifier for 'separated'                                         --- *)
+(* -------------------------------------------------------------------------- *)
+
+let r_separated = function
+  | [p;a;q;b] ->
+    if a == e_one && b == e_one then e_neq p q
+    else
+      begin
+        let a_negative = e_leq a e_zero in
+        let b_negative = e_leq b e_zero in
+        if a_negative == e_true || b_negative == e_true then e_true else
+          let bp = base p in
+          let bq = base q in
+          match is_true (e_eq bp bq) with
+          | No -> e_true (* Have S *)
+          | Yes when (a_negative == e_false && b_negative == e_false) ->
+            (* Reduced to S *)
+            let p_ofs = offset p in
+            let q_ofs = offset q in
+            let p_ofs' = e_add p_ofs a in
+            let q_ofs' = e_add q_ofs b in
+            e_or [ e_leq q_ofs' p_ofs ;
+                   e_leq p_ofs' q_ofs ]
+          | _ -> raise Not_found
+      end
+  | _ -> raise Not_found
+
+let is_separated args = is_true (r_separated args)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Simplifier for 'included'                                          --- *)
+(* -------------------------------------------------------------------------- *)
+
+(* See: tests/why3/test_memory.why
+
+   logic a : int
+   logic b : int
+
+   predicate R = p.base = q.base
+              /\ (q.offset <= p.offset)
+              /\ (p.offset + a <= q.offset + b)
+
+   predicate included = 0 < a -> ( 0 <= b and R )
+   predicate a_empty = a <= 0
+   predicate b_negative = b < 0
+
+   lemma SAME_P: p=q -> (R <-> a<=b)
+   lemma SAME_A: a=b -> (R <-> p=q)
+
+   goal INC_P:  p=q -> (included <-> ( 0 < a -> a <= b )) (by SAME_P)
+   goal INC_A:  a=b -> 0 < a -> (included <-> R) (by SAME_A)
+   goal INC_1:  a_empty -> (included <-> true)
+   goal INC_2:  b_negative -> (included <-> a_empty)
+   goal INC_3:  not R -> (included <-> a_empty)
+   goal INC_4:  not a_empty -> not b_negative -> (included <-> R)
+*)
+
+let r_included = function
+  | [p;a;q;b] ->
+    if e_eq p q == e_true
+    then e_imply [e_lt e_zero a] (e_leq a b) (* INC_P *)
+    else
+    if (e_eq a b == e_true) && (e_lt e_zero a == e_true)
+    then e_eq p q (* INC_A *)
+    else
+      begin
+        let a_empty = e_leq a e_zero in
+        let b_negative = e_lt b e_zero in
+        if a_empty == e_true then e_true (* INC_1 *) else
+        if b_negative == e_true then a_empty (* INC_2 *) else
+          let bp = base p in
+          let bq = base q in
+          match is_true (e_eq bp bq) with
+          | No -> a_empty (* INC_3 *)
+          | Yes when (a_empty == e_false && b_negative == e_false) ->
+            (* INC_4 *)
+            let p_ofs = offset p in
+            let q_ofs = offset q in
+            if a == b then e_eq p_ofs q_ofs
+            else
+              let p_ofs' = e_add p_ofs a in
+              let q_ofs' = e_add q_ofs b in
+              e_and [ e_leq q_ofs p_ofs ; e_leq p_ofs' q_ofs' ]
+          | _ -> raise Not_found
+      end
+  | _ -> raise Not_found
+
+let is_included args = is_true (r_included args)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Simplifier for int/addr conversion                                 --- *)
+(* -------------------------------------------------------------------------- *)
+
+let phi_int_of_addr p =
+  if p == null then e_zero else
+    match repr p with
+    | Fun(f,[a]) when f == f_addr_of_int -> a
+    | _ -> raise Not_found
+
+let phi_addr_of_int p =
+  if p == e_zero then null else
+    match repr p with
+    | Fun(f,[a]) when f == f_int_of_addr -> a
+    | _ -> raise Not_found
+
+(* -------------------------------------------------------------------------- *)
+(* --- Simplifier for (in)validity                                        --- *)
+(* -------------------------------------------------------------------------- *)
+
+let null_base p = e_eq (e_fun f_base [p]) e_zero
+
+(* See: tests/why3/test_memory.why *)
+
+(* - lemma valid_rd_null: forall m n p. p.base = 0 -> (n <= 0 <-> valid_rd m p n)
+   - lemma valid_rw_null: forall m n p. p.base = 0 -> (n <= 0 <-> valid_rw m p n)
+*)
+let r_valid_unref = function
+  | [_; p; n] when decide (null_base p) ->
+    e_leq n e_zero
+  | _ -> raise Not_found
+
+(* - lemma valid_obj_null: forall m n. valid_obj m null n *)
+let r_valid_obj = function
+  | [_; p; _] when decide (e_eq p null) -> e_true
+  | _ -> raise Not_found
+
+(* - lemma invalid_null: forall m n p. p.base = 0 -> invalid m p n *)
+let r_invalid = function
+  | [_; p; _] when decide (null_base p) -> e_true
+  | _ -> raise Not_found
+
+(* -------------------------------------------------------------------------- *)
+(* --- Simplifiers Registration                                           --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () = Context.register
+    begin fun () ->
+      set_builtin_1   f_base   phi_base ;
+      set_builtin_1   f_offset phi_offset ;
+      set_builtin_2   f_shift  (phi_shift f_shift) ;
+      set_builtin_eqp f_shift  eq_shift ;
+      set_builtin_eqp f_global eq_shift ;
+      set_builtin p_separated r_separated ;
+      set_builtin p_included  r_included ;
+      set_builtin_1 f_addr_of_int phi_addr_of_int ;
+      set_builtin_1 f_int_of_addr phi_int_of_addr ;
+      set_builtin p_invalid r_invalid ;
+      set_builtin p_valid_rd r_valid_unref ;
+      set_builtin p_valid_rw r_valid_unref ;
+      set_builtin p_valid_obj r_valid_obj ;
+    end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Identify lfun                                                      --- *)
+(* -------------------------------------------------------------------------- *)
+
+let is_p_valid_rd lf = lf == p_valid_rd
+let is_p_valid_rw lf = lf == p_valid_rw
+let is_p_valid_obj lf = lf == p_valid_obj
+let is_p_invalid lf = lf == p_invalid
+
+let is_f_global lf = lf == f_global
+
+(* -------------------------------------------------------------------------- *)
+(* --- Range Comparison                                                   --- *)
+(* -------------------------------------------------------------------------- *)
+
+type range =
+  | LOC of term * term (* loc - size *)
+  | RANGE of term * Vset.set (* base - range offset *)
+
+let range ~shift ~addrof ~sizeof = function
+  | Sigs.Rloc(obj,loc) ->
+    LOC( addrof loc , sizeof obj )
+  | Sigs.Rrange(loc,obj,Some a,Some b) ->
+    let s = sizeof obj in
+    let p = addrof (shift loc obj a) in
+    let n = e_mul s (e_range a b) in
+    LOC( p , n )
+  | Sigs.Rrange(loc,_obj,None,None) ->
+    RANGE( base (addrof loc) , Vset.range None None )
+  | Sigs.Rrange(loc,obj,Some a,None) ->
+    let s = sizeof obj in
+    RANGE( base (addrof loc) , Vset.range (Some (e_mul s a)) None )
+  | Sigs.Rrange(loc,obj,None,Some b) ->
+    let s = sizeof obj in
+    RANGE( base (addrof loc) , Vset.range None (Some (e_mul s b)) )
+
+let range_set = function
+  | LOC(l,n) ->
+    let a = offset l in
+    let b = e_add a n in
+    base l , Vset.range (Some a) (Some b)
+  | RANGE(base,set) -> base , set
+
+let r_included r1 r2 =
+  match r1 , r2 with
+  | LOC(l1,n1) , LOC(l2,n2) ->
+    p_call p_included [l1;n1;l2;n2]
+  | _ ->
+    let base1,set1 = range_set r1 in
+    let base2,set2 = range_set r2 in
+    p_if (p_equal base1 base2)
+      (Vset.subset set1 set2)
+      (Vset.is_empty set1)
+
+let r_disjoint r1 r2 =
+  match r1 , r2 with
+  | LOC(l1,n1) , LOC(l2,n2) ->
+    p_call p_separated [l1;n1;l2;n2]
+  | _ ->
+    let base1,set1 = range_set r1 in
+    let base2,set2 = range_set r2 in
+    p_imply (p_equal base1 base2) (Vset.disjoint set1 set2)
+
+let included ~shift ~addrof ~sizeof s1 s2  =
+  let range = range ~shift ~addrof ~sizeof in
+  r_included (range s1) (range s2)
+
+let separated ~shift ~addrof ~sizeof s1 s2 =
+  let range = range ~shift ~addrof ~sizeof in
+  r_disjoint (range s1) (range s2)
diff --git a/src/plugins/wp/MemAddr.mli b/src/plugins/wp/MemAddr.mli
new file mode 100644
index 0000000000000000000000000000000000000000..38f30863eaffcb38353aa83fddbd8afbeb0572f5
--- /dev/null
+++ b/src/plugins/wp/MemAddr.mli
@@ -0,0 +1,166 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of WP plug-in of Frama-C.                           *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2023                                               *)
+(*    CEA (Commissariat a l'energie atomique et aux energies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Lang.F
+
+(** Smart-constructors for building Qed terms from the MemAddr Why3 module
+    symbols. Types indicates in the documentation are Why3 types, not OCaml
+    types.
+
+    @since Frama-C+dev
+*)
+
+val t_addr : Lang.tau
+(** Pointer type : addr *)
+
+(** {2 Basic constructors} *)
+
+val base : term -> term
+(** [base(a: addr) : int = a.base] *)
+
+val offset : term -> term
+(** [offset(a: addr) : int = a.offset] *)
+
+val null : term
+(** [null : addr = { base = 0 ; offset = 0 }] *)
+
+val mk_addr : term -> term -> term
+(** [mk_addr(base: int)(offset: int) : addr = { base ; offset }] *)
+
+val global : term -> term
+(** [global(base: int) : addr = { base ; offset = 0 }] *)
+
+val shift : term -> term -> term
+(** [shift (a: addr) (k: int) : addr = { a with offset = a.offset + k } ]*)
+
+val addr_lt : term -> term -> pred
+(** [addr_lt(a: addr) (b: addr) = a < b] *)
+
+val addr_le : term -> term -> pred
+(** [addr_le(a: addr) (b: addr) = a <= b] *)
+
+val addr_of_int : term -> term
+(** [addr_of_int(i: int) : addr]
+    Abstract: Conversion from integer to address
+*)
+
+val int_of_addr : term -> term
+(** [int_of_addr (a: addr) : int]
+    Abstract: Conversion from address to integer
+*)
+
+val base_offset : term -> term -> term
+(** [base_offset(base: int)(offset: int) : int]
+    Converts a {i logic} offset (which is actually the address of a memory cell
+    in a given memory model into an offset in {i bytes}.
+*)
+
+(** {2 Symbols related to the table of allocation (int -> int)} *)
+
+val valid_rd : term -> term -> term -> pred
+(** [valid_rd(m: malloc)(a: addr)(l: length)] *)
+
+val valid_rw : term -> term -> term -> pred
+(** [valid_rw(m: malloc)(a: addr)(l: length)] *)
+
+val valid_obj : term -> term -> term -> pred
+(** [valid_obj(m: malloc)(a: addr)(l: length)] *)
+
+val invalid : term -> term -> term -> pred
+(** [invalid(m: malloc)(a: addr)(l: length)]
+    Invalidity means that the {i entire} range of addresses is invalid.
+*)
+
+val region : term -> term
+(** [region(base: int) : int]
+    The memory region a base belongs to.
+*)
+
+val linked : term -> pred
+(** [linked(m: malloc)] *)
+
+val register :
+  ?base:(term list -> term) ->
+  ?offset:(term list -> term) ->
+  ?equal:(term -> term -> pred) ->
+  ?linear:bool -> Lang.lfun -> unit
+(** Register simplifiers for functions producing [addr] terms:
+    - [~base es] is the simplifier for [(f es).base]
+    - [~offset es] is the simplifier for [(f es).offset]
+    - [~linear:true] register simplifier [f(f(p,i),k)=f(p,i+j)] on [f]
+    - [~equal a b] is the [set_eq_builtin] for [f]
+
+    The equality builtin is wrapped inside a default builtin that
+    compares [f es] by computing [base] and [offset].
+*)
+
+(** {2 Memory model parameterized inclusion and separation} *)
+
+val included :
+  shift:('loc -> Ctypes.c_object -> term -> 'loc) ->
+  addrof:('loc -> term) ->
+  sizeof:(Ctypes.c_object -> term) ->
+  'loc Sigs.rloc -> 'loc Sigs.rloc -> pred
+(** [included ~shift ~addrof ~sizeof r1 r2] builds a predicate that checks
+    whether [r1] is included in [r2].
+    - [shift loc obj k]: [loc] shifted of [k] [obj] in the memory model,
+    - [addrof loc]: [loc] translated into a [term] in the memory model,
+    - [sizeof obj]: the length of [obj] in the memory model.
+*)
+
+val separated :
+  shift:('loc -> Ctypes.c_object -> term -> 'loc) ->
+  addrof:('loc -> term) ->
+  sizeof:(Ctypes.c_object -> term) ->
+  'loc Sigs.rloc -> 'loc Sigs.rloc -> pred
+(** [separated ~shift ~addrof ~sizeof r1 r2] builds a predicate that checks
+    whether [r1] and [r2] are separated.
+    - [shift loc obj k]: [loc] shifted of [k] [obj] in the memory model,
+    - [addrof loc]: [loc] translated into a [term] in the memory model,
+    - [sizeof obj]: the length of [obj] in the memory model.
+*)
+
+(** {2 Qed symbols identification} *)
+
+val is_p_valid_rd  : Lang.lfun -> bool
+val is_p_valid_rw  : Lang.lfun -> bool
+val is_p_valid_obj : Lang.lfun -> bool
+val is_p_invalid   : Lang.lfun -> bool
+val is_f_global    : Lang.lfun -> bool
+
+(** {2 Raw Qed symbols} *)
+(** Use them with care, for building terms, prefer above constructors *)
+
+val p_separated : Lang.lfun
+val p_included : Lang.lfun
+
+(** {2 Qed simplification procedures} *)
+
+val is_separated : term list -> Qed.Logic.maybe
+(** [is_separated [ a ; la ; b ; lb ]]
+    Try to solve with Qed that separated(a, la, b, lb)
+*)
+
+val is_included : term list -> Qed.Logic.maybe
+(** [is_included [ a ; la ; b ; lb ]]
+    Try to solve with Qed that included(a, la, b, lb)
+*)
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index 062e3f01e3ebd9ee90fcdb40141fbc3975d2f92d..8ad0a096b7583126cd52c328954968b306f2d9fe 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -31,25 +31,6 @@ module L = Qed.Logic
 
 let library = "memory"
 
-let a_addr = Lang.datatype ~library "addr"
-let t_addr = L.Data(a_addr,[])
-let f_base   = Lang.extern_f ~library ~result:L.Int
-    ~link:(Qed.Engine.F_subst ("base", "%1.base")) "base"
-let f_offset = Lang.extern_f ~library ~result:L.Int
-    ~link:(Qed.Engine.F_subst ("offset", "%1.offset")) "offset"
-let f_shift  = Lang.extern_f ~library ~result:t_addr "shift"
-let f_global = Lang.extern_f ~library ~result:t_addr ~category:L.Injection "global"
-let f_null   = Lang.extern_f ~library ~result:t_addr "null"
-
-let a_table = Lang.datatype ~library "table"
-let t_table = L.Data(a_table,[])
-
-let f_table_of_base = Lang.extern_f ~library
-    ~category:Qed.Logic.Function ~result:t_table "table_of_base"
-
-let f_table_to_offset = Lang.extern_f ~library
-    ~category:Qed.Logic.Injection ~result:L.Int "table_to_offset"
-
 let ty_fst_arg = function
   | Some l :: _ -> l
   | _ -> raise Not_found
@@ -57,227 +38,27 @@ let ty_fst_arg = function
 let l_havoc = Qed.Engine.F_call "havoc"
 let l_set_init = Qed.Engine.F_call "set_init"
 
-let p_valid_rd = Lang.extern_fp ~library "valid_rd"
-let p_valid_rw = Lang.extern_fp ~library "valid_rw"
-let p_valid_obj = Lang.extern_fp ~library "valid_obj"
-let p_invalid = Lang.extern_fp ~library "invalid"
-let p_separated = Lang.extern_fp ~library "separated"
-let p_included = Lang.extern_fp ~library "included"
 let p_eqmem = Lang.extern_fp ~library "eqmem"
 let f_havoc = Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_havoc "havoc"
-let f_region = Lang.extern_f ~coloring:true ~library ~result:L.Int "region" (* base -> region *)
 let p_framed = Lang.extern_fp ~coloring:true ~library "framed" (* m-pointer -> prop *)
-let p_linked = Lang.extern_fp ~coloring:true ~library "linked" (* allocation-table -> prop *)
 let p_sconst = Lang.extern_fp ~coloring:true ~library "sconst" (* int-memory -> prop *)
-let p_addr_lt = Lang.extern_p ~library ~bool:"addr_lt_bool" ~prop:"addr_lt" ()
-let p_addr_le = Lang.extern_p ~library ~bool:"addr_le_bool" ~prop:"addr_le" ()
 let f_set_init =
   Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_set_init "set_init"
 let p_cinits = Lang.extern_fp ~coloring:true ~library "cinits" (* initializaton-table -> prop *)
 let p_is_init_r = Lang.extern_fp ~library "is_init_range"
 let p_monotonic = Lang.extern_fp ~library "monotonic_init"
 
-let f_addr_of_int = Lang.extern_f
-    ~category:L.Injection
-    ~library ~result:t_addr "addr_of_int"
-
-let f_int_of_addr = Lang.extern_f
-    ~category:L.Injection
-    ~library ~result:L.Int "int_of_addr"
-
 (* -------------------------------------------------------------------------- *)
 (* --- Utilities                                                          --- *)
 (* -------------------------------------------------------------------------- *)
 
-let t_mem t = L.Array(t_addr,t)
+let t_mem t = L.Array(MemAddr.t_addr,t)
 let t_malloc = L.Array(L.Int,L.Int)
-let t_init = L.Array(t_addr,L.Bool)
-
-let a_null = F.constant (e_fun f_null [])
-let a_base p = e_fun f_base [p]
-let a_offset p = e_fun f_offset [p]
-let a_global b = e_fun f_global [b]
-let a_shift l k = e_fun f_shift [l;k]
-let a_addr b k = a_shift (a_global b) k
-let a_base_offset b k =
-  let offset_index = e_fun f_table_of_base [b] in
-  e_fun f_table_to_offset [offset_index ; k]
-
-(* -------------------------------------------------------------------------- *)
-(* --- Qed Simplifiers                                                    --- *)
-(* -------------------------------------------------------------------------- *)
-
-(*
-    Pointer arithmetic for structure access and array access could be
-    defined directly using the record [{ base = p.base; offset = p.offset
-    + c*i + c' }]. However that gives very bad triggers for the memory
-    model axiomatization, so `shift p (c*i+c')` was used instead. It is
-    not sufficient for user axiomatisation because memory access in
-    axioms require trigger with arithmetic operators which is badly
-    handled by provers. So for each c and c', ie for each kind of
-    structure access and array access a specific function is used
-    `shift_xxx`.
-
-    Moreover no simplification of `shift_xxx` is done for keeping the
-    same terms in axioms and the goal. `base` and `offset` function
-    simplify all the `shift_xxx` because it seems they don't appear
-    often in axioms and they are useful for simplifying `separated`,
-    `assigns` and pointer comparisons in goals.
-
-    To sum up memory access should match, but not `\base`, `\offset`,
-    `\separated`, ...
-*)
-
-type addr_builtin = {
-  base: term list -> term ;
-  offset: term list -> term ;
-}
-
-module ADDR_BUILTIN = WpContext.Static
-    (struct
-      type key = lfun
-      type data = addr_builtin
-      let name = "MemMemory.ADDR_BUILTIN"
-      include Lang.Fun
-    end)
-
-let phi_base l =
-  match F.repr l with
-  | L.Fun(f,[p;_]) when f==f_shift -> a_base p
-  | L.Fun(f,[b]) when f==f_global -> b
-  | L.Fun(f,[]) when f==f_null -> e_zero
-  | L.Fun(f,args) -> (ADDR_BUILTIN.find f).base args
-  | _ -> raise Not_found
-
-let phi_offset l = match F.repr l with
-  | L.Fun(f,[p;k]) when f==f_shift -> e_add (a_offset p) k
-  | L.Fun(f,_) when f==f_global || f==f_null -> F.e_zero
-  | L.Fun(f,args) -> (ADDR_BUILTIN.find f).offset args
-  | _ -> raise Not_found
-
-let phi_shift f p i =
-  match F.repr p with
-  | L.Fun(g,[q;j]) when f == g -> F.e_fun f [q;F.e_add i j]
-  | _ -> raise Not_found
-
-let eq_shift a b =
-  let p = a_base a in
-  let q = a_base b in
-  let i = a_offset a in
-  let j = a_offset b in
-  if i==j then F.p_equal p q else
-    match F.is_equal p q with
-    | L.No -> F.p_false
-    | L.Yes -> F.p_equal i j
-    | L.Maybe -> raise Not_found
-
-let eq_shift_gen phi a b =
-  try phi a b with Not_found -> eq_shift a b
-
-let nop _ = raise Not_found
-
-let register ?(base=nop) ?(offset=nop) ?equal ?(linear=false) lfun =
-  begin
-    if base != nop || offset != nop then
-      ADDR_BUILTIN.define lfun { base ; offset } ;
-    if linear then
-      F.set_builtin_2 lfun (phi_shift lfun) ;
-    let phi_equal = match equal with
-      | None -> eq_shift
-      | Some phi -> eq_shift_gen phi
-    in
-    F.set_builtin_eqp lfun phi_equal ;
-  end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Simplifier for 'separated'                                         --- *)
-(* -------------------------------------------------------------------------- *)
-
-let r_separated = function
-  | [p;a;q;b] ->
-    if a == F.e_one && b == F.e_one then F.e_neq p q
-    else
-      begin
-        let a_negative = F.e_leq a F.e_zero in
-        let b_negative = F.e_leq b F.e_zero in
-        if a_negative == e_true || b_negative == e_true then e_true else
-          let bp = a_base p in
-          let bq = a_base q in
-          let open Qed.Logic in
-          match F.is_true (F.e_eq bp bq) with
-          | No -> e_true (* Have S *)
-          | Yes when (a_negative == e_false && b_negative == e_false) ->
-            (* Reduced to S *)
-            let p_ofs = a_offset p in
-            let q_ofs = a_offset q in
-            let p_ofs' = F.e_add p_ofs a in
-            let q_ofs' = F.e_add q_ofs b in
-            F.e_or [ F.e_leq q_ofs' p_ofs ;
-                     F.e_leq p_ofs' q_ofs ]
-          | _ -> raise Not_found
-      end
-  | _ -> raise Not_found
-
-let is_separated args = F.is_true (r_separated args)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Simplifier for 'included'                                          --- *)
-(* -------------------------------------------------------------------------- *)
+let t_init = L.Array(MemAddr.t_addr,L.Bool)
 
-(* See: tests/why3/test_memory.why
-
-   logic a : int
-   logic b : int
-
-   predicate R = p.base = q.base
-              /\ (q.offset <= p.offset)
-              /\ (p.offset + a <= q.offset + b)
-
-   predicate included = 0 < a -> ( 0 <= b and R )
-   predicate a_empty = a <= 0
-   predicate b_negative = b < 0
-
-   lemma SAME_P: p=q -> (R <-> a<=b)
-   lemma SAME_A: a=b -> (R <-> p=q)
-
-   goal INC_P:  p=q -> (included <-> ( 0 < a -> a <= b )) (by SAME_P)
-   goal INC_A:  a=b -> 0 < a -> (included <-> R) (by SAME_A)
-   goal INC_1:  a_empty -> (included <-> true)
-   goal INC_2:  b_negative -> (included <-> a_empty)
-   goal INC_3:  not R -> (included <-> a_empty)
-   goal INC_4:  not a_empty -> not b_negative -> (included <-> R)
-*)
-
-let r_included = function
-  | [p;a;q;b] ->
-    if F.e_eq p q == F.e_true
-    then F.e_imply [F.e_lt F.e_zero a] (F.e_leq a b) (* INC_P *)
-    else
-    if (F.e_eq a b == F.e_true) && (F.e_lt F.e_zero a == F.e_true)
-    then F.e_eq p q (* INC_A *)
-    else
-      begin
-        let a_empty = F.e_leq a F.e_zero in
-        let b_negative = F.e_lt b F.e_zero in
-        if a_empty == F.e_true then F.e_true (* INC_1 *) else
-        if b_negative == F.e_true then a_empty (* INC_2 *) else
-          let bp = a_base p in
-          let bq = a_base q in
-          let open Qed.Logic in
-          match F.is_true (F.e_eq bp bq) with
-          | No -> a_empty (* INC_3 *)
-          | Yes when (a_empty == e_false && b_negative == e_false) ->
-            (* INC_4 *)
-            let p_ofs = a_offset p in
-            let q_ofs = a_offset q in
-            if a == b then F.e_eq p_ofs q_ofs
-            else
-              let p_ofs' = e_add p_ofs a in
-              let q_ofs' = e_add q_ofs b in
-              e_and [ F.e_leq q_ofs p_ofs ; F.e_leq p_ofs' q_ofs' ]
-          | _ -> raise Not_found
-      end
-  | _ -> raise Not_found
+let cinits memory = p_call p_cinits [ memory ]
+let sconst memory = p_call p_sconst [ memory ]
+let framed memory = p_call p_framed [ memory ]
 
 (* -------------------------------------------------------------------------- *)
 (* --- Simplifier for 'havoc'                                             --- *)
@@ -290,7 +71,7 @@ let r_havoc = function
       match F.repr m1 with
       | L.Fun( f , [_undef0;m0;p0;a0] ) when f == f_havoc -> begin
           let open Qed.Logic in
-          match F.is_true (r_included [p0;a0;p1;a1]) with
+          match MemAddr.is_included [p0;a0;p1;a1] with
           | Yes -> F.e_fun f_havoc [undef1;m0;p1;a1]
           | _ -> raise Not_found
         end
@@ -306,76 +87,21 @@ let r_get_havoc es ks =
   match es, ks with
   | [undef;m;p;a],[k] ->
     begin
-      match is_separated [p;a;k;e_one] with
+      match MemAddr.is_separated [p;a;k;e_one] with
       | L.Yes -> F.e_get m k
       | L.No  -> F.e_get undef k
       | _ -> raise Not_found
     end
   | _ -> raise Not_found
 
-(* -------------------------------------------------------------------------- *)
-(* --- Simplifier for int/addr conversion                                 --- *)
-(* -------------------------------------------------------------------------- *)
-
-let phi_int_of_addr p =
-  if p == a_null then F.e_zero else
-    match F.repr p with
-    | L.Fun(f,[a]) when f == f_addr_of_int -> a
-    | _ -> raise Not_found
-
-let phi_addr_of_int p =
-  if p == F.e_zero then a_null else
-    match F.repr p with
-    | L.Fun(f,[a]) when f == f_int_of_addr -> a
-    | _ -> raise Not_found
-
-(* -------------------------------------------------------------------------- *)
-(* --- Simplifier for (in)validity                                        --- *)
-(* -------------------------------------------------------------------------- *)
-
-let null_base p = e_eq (F.e_fun f_base [p]) F.e_zero
-
-(* See: tests/why3/test_memory.why *)
-
-(* - lemma valid_rd_null: forall m n p. p.base = 0 -> (n <= 0 <-> valid_rd m p n)
-   - lemma valid_rw_null: forall m n p. p.base = 0 -> (n <= 0 <-> valid_rw m p n)
-*)
-let r_valid_unref = function
-  | [_; p; n] when F.decide (null_base p) ->
-    e_leq n e_zero
-  | _ -> raise Not_found
-
-(* - lemma valid_obj_null: forall m n. valid_obj m null n *)
-let r_valid_obj = function
-  | [_; p; _] when F.decide (e_eq p a_null) -> e_true
-  | _ -> raise Not_found
-
-(* - lemma invalid_null: forall m n p. p.base = 0 -> invalid m p n *)
-let r_invalid = function
-  | [_; p; _] when F.decide (null_base p) -> e_true
-  | _ -> raise Not_found
-
 (* -------------------------------------------------------------------------- *)
 (* --- Simplifiers Registration                                           --- *)
 (* -------------------------------------------------------------------------- *)
 
 let () = Context.register
     begin fun () ->
-      F.set_builtin_1   f_base   phi_base ;
-      F.set_builtin_1   f_offset phi_offset ;
-      F.set_builtin_2   f_shift  (phi_shift f_shift) ;
-      F.set_builtin_eqp f_shift  eq_shift ;
-      F.set_builtin_eqp f_global eq_shift ;
-      F.set_builtin p_separated r_separated ;
-      F.set_builtin p_included  r_included ;
       F.set_builtin f_havoc r_havoc ;
       F.set_builtin_get f_havoc r_get_havoc ;
-      F.set_builtin_1 f_addr_of_int phi_addr_of_int ;
-      F.set_builtin_1 f_int_of_addr phi_int_of_addr ;
-      F.set_builtin p_invalid r_invalid ;
-      F.set_builtin p_valid_rd r_valid_unref ;
-      F.set_builtin p_valid_rw r_valid_unref ;
-      F.set_builtin p_valid_obj r_valid_obj ;
     end
 
 (* -------------------------------------------------------------------------- *)
@@ -385,17 +111,17 @@ let () = Context.register
 module T = Definitions.Trigger
 
 let frames ~addr:p ~offset:n ~sizeof:s ?(basename="mem") tau =
-  let t_mem = L.Array(t_addr,tau) in
+  let t_mem = L.Array(MemAddr.t_addr,tau) in
   let m  = F.e_var (Lang.freshvar ~basename t_mem) in
   let m' = F.e_var (Lang.freshvar ~basename t_mem) in
-  let p' = F.e_var (Lang.freshvar ~basename:"q" t_addr) in
+  let p' = F.e_var (Lang.freshvar ~basename:"q" MemAddr.t_addr) in
   let n' = F.e_var (Lang.freshvar ~basename:"n" L.Int) in
   let mh = F.e_fun f_havoc [m';m;p';n'] in
   let v' = F.e_var (Lang.freshvar ~basename:"v" tau) in
   let meq = F.p_call p_eqmem [m;m';p';n'] in
-  let diff = F.p_call p_separated [p;n;p';s] in
-  let sep = F.p_call p_separated [p;n;p';n'] in
-  let inc = F.p_call p_included [p;n;p';n'] in
+  let diff = F.p_call MemAddr.p_separated [p;n;p';s] in
+  let sep = F.p_call MemAddr.p_separated [p;n;p';n'] in
+  let inc = F.p_call MemAddr.p_included [p;n;p';n'] in
   let teq = T.of_pred meq in
   [
     "update" , [] , [diff] , m , e_set m p' v' ;
@@ -403,66 +129,6 @@ let frames ~addr:p ~offset:n ~sizeof:s ?(basename="mem") tau =
     "havoc" , [] , [sep] , m , mh ;
   ]
 
-(* -------------------------------------------------------------------------- *)
-(* --- Range Comparison                                                   --- *)
-(* -------------------------------------------------------------------------- *)
-
-type range =
-  | LOC of term * term (* loc - size *)
-  | RANGE of term * Vset.set (* base - range offset *)
-
-let range ~shift ~addrof ~sizeof = function
-  | Sigs.Rloc(obj,loc) ->
-    LOC( addrof loc , sizeof obj )
-  | Sigs.Rrange(loc,obj,Some a,Some b) ->
-    let s = sizeof obj in
-    let p = addrof (shift loc obj a) in
-    let n = e_mul s (e_range a b) in
-    LOC( p , n )
-  | Sigs.Rrange(loc,_obj,None,None) ->
-    RANGE( a_base (addrof loc) , Vset.range None None )
-  | Sigs.Rrange(loc,obj,Some a,None) ->
-    let s = sizeof obj in
-    RANGE( a_base (addrof loc) , Vset.range (Some (e_mul s a)) None )
-  | Sigs.Rrange(loc,obj,None,Some b) ->
-    let s = sizeof obj in
-    RANGE( a_base (addrof loc) , Vset.range None (Some (e_mul s b)) )
-
-let range_set = function
-  | LOC(l,n) ->
-    let a = a_offset l in
-    let b = e_add a n in
-    a_base l , Vset.range (Some a) (Some b)
-  | RANGE(base,set) -> base , set
-
-let r_included r1 r2 =
-  match r1 , r2 with
-  | LOC(l1,n1) , LOC(l2,n2) ->
-    F.p_call p_included [l1;n1;l2;n2]
-  | _ ->
-    let base1,set1 = range_set r1 in
-    let base2,set2 = range_set r2 in
-    F.p_if (F.p_equal base1 base2)
-      (Vset.subset set1 set2)
-      (Vset.is_empty set1)
-
-let r_disjoint r1 r2 =
-  match r1 , r2 with
-  | LOC(l1,n1) , LOC(l2,n2) ->
-    F.p_call p_separated [l1;n1;l2;n2]
-  | _ ->
-    let base1,set1 = range_set r1 in
-    let base2,set2 = range_set r2 in
-    F.p_imply (F.p_equal base1 base2) (Vset.disjoint set1 set2)
-
-let included ~shift ~addrof ~sizeof s1 s2  =
-  let range = range ~shift ~addrof ~sizeof in
-  r_included (range s1) (range s2)
-
-let separated ~shift ~addrof ~sizeof s1 s2 =
-  let range = range ~shift ~addrof ~sizeof in
-  r_disjoint (range s1) (range s2)
-
 (* -------------------------------------------------------------------------- *)
 (* --- Unsupported Unions                                                 --- *)
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/MemMemory.mli b/src/plugins/wp/MemMemory.mli
index 094cbb0bdc479fa0e6ced313eafc9449dccf740d..220b4e82b881c14817dc2280ed79f5abd38d7b7e 100644
--- a/src/plugins/wp/MemMemory.mli
+++ b/src/plugins/wp/MemMemory.mli
@@ -29,82 +29,24 @@ open Lang.F
 
 (** {2 Theory} *)
 
-val t_addr : tau
 val t_malloc : tau (** allocation tables *)
 
 val t_init : tau (** initialization tables *)
 
 val t_mem : tau -> tau (** t_addr indexed array *)
 
-val a_null : term (** Null address. Same as [a_addr 0 0] *)
-
-val a_global : term -> term (** Zero-offset base. Same as [a_addr base 0] *)
-
-val a_addr : term -> term -> term (** Constructor for [{ base ; offset }] *)
-
-val a_shift : term -> term -> term
-(** Shift: [a_shift a k] adds [k] to [a.offset] *)
-
-val a_base : term -> term
-(** Returns the base *)
-
-val a_offset : term -> term
-(** Returns the offset *)
-
-val a_base_offset : term -> term -> term
-(** Returns the offset in {i bytes} from the {i logic} offset
-    (which is a memory cell index, actually) *)
-
-val f_null : lfun
-val f_base : lfun
-val f_global : lfun
-val f_shift : lfun
-val f_offset : lfun
 val f_havoc : lfun
 val f_set_init : lfun
-val f_region : lfun
-
-val f_addr_of_int : lfun (** Physical address *)
 
-val f_int_of_addr : lfun (** Physical address *)
-
-val p_addr_lt : lfun
-val p_addr_le : lfun
-val p_linked : lfun
-val p_framed : lfun
-val p_sconst : lfun
-val p_cinits : lfun
 val p_is_init_r : lfun
-val p_separated : lfun
-val p_included : lfun
-val p_valid_rd : lfun
-val p_valid_rw : lfun
-val p_valid_obj : lfun
-val p_invalid : lfun
 val p_eqmem : lfun
 val p_monotonic : lfun
 
-(* -------------------------------------------------------------------------- *)
-
-(** {2 Addr Producer Registration} *)
-
-(** Register simplifiers for functions producing [addr] terms:
-    - [~base es] is the simplifier for [(f es).base]
-    - [~offset es] is the simplifier for [(f es).offset]
-    - [~linear:true] register simplifier [f(f(p,i),k)=f(p,i+j)] on [f]
-    - [~equal a b] is the [set_eq_builtin] for [f]
-
-    The equality builtin is wrapped inside a default builtin that
-    compares [f es] by computing [base] and [offset].
-*)
-
-val register :
-  ?base:(term list -> term) ->
-  ?offset:(term list -> term) ->
-  ?equal:(term -> term -> pred) ->
-  ?linear:bool ->
-  lfun -> unit
+val cinits : term -> pred
+val sconst : term -> pred
+val framed : term -> pred
 
+(* -------------------------------------------------------------------------- *)
 
 (** {2 Frame Conditions}
 
@@ -120,20 +62,6 @@ val register :
 val frames : addr:term -> offset:term -> sizeof:term ->
   ?basename:string -> tau -> Sigs.frame list
 
-(** {2 Range of Address} *)
-
-val separated :
-  shift:('a -> Ctypes.c_object -> term -> 'a) ->
-  addrof:('a -> term) ->
-  sizeof:(Ctypes.c_object -> term) ->
-  'a Sigs.rloc -> 'a Sigs.rloc -> pred
-
-val included :
-  shift:('a -> Ctypes.c_object -> term -> 'a) ->
-  addrof:('a -> term) ->
-  sizeof:(Ctypes.c_object -> term) ->
-  'a Sigs.rloc -> 'a Sigs.rloc -> pred
-
 (** {2 Unsupported Union Fields} *)
 
 val unsupported_union : Cil_types.fieldinfo -> unit
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index c6498e3b539ea64a14698393fbdf91e8815d00a6..0c1f75690761fb479909a7b6a646b2a79dc2d8f2 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -45,7 +45,7 @@ let cluster_region () =
   Definitions.cluster ~id:"Region" ~title:"Region Index Constructors" ()
 
 (* Index *)
-let t_addr = MemMemory.t_addr
+let t_addr = MemAddr.t_addr
 let t_index = L.Data( Lang.datatype ~library "index" ,[] )
 let f_addrof = Lang.extern_f ~library ~result:t_addr "addrof"
 let f_consistent = Lang.extern_fp ~library "consistent"
@@ -59,12 +59,7 @@ let p_range k n ps = F.(p_leq e_zero k :: p_lt k n :: ps)
 (* Null *)
 let f_inull = Lang.extern_f ~library ~result:t_index "inull"
 let l_inull = F.e_fun f_inull []
-let a_null = MemMemory.a_null
-let p_inull l = F.p_equal a_null (a_addrof l)
-
-(* Address *)
-
-let p_separated p n q m = F.p_call MemMemory.p_separated [p;n;q;m]
+let p_inull l = F.p_equal MemAddr.null (a_addrof l)
 
 (* Constructors *)
 let region_ctor ~result =
@@ -86,7 +81,6 @@ let l_index_ref l = F.e_fun f_index_ref [l]
 
 (* Shifts *)
 
-let a_shift = MemMemory.a_shift
 let f_shift_index = Lang.extern_f ~library ~result:t_index "shift_index"
 let l_shift_index l p = F.e_fun f_shift_index [l;p]
 
@@ -120,10 +114,10 @@ let is_shiftable f =
 
 let phi_addrof index =
   match F.repr index with
-  | L.Fun(f,[]) when f == f_inull -> a_null
+  | L.Fun(f,[]) when f == f_inull -> MemAddr.null
   | L.Fun(f,[x]) when f == f_index_var -> a_addr_var x
   | L.Fun(f,[l]) when f == f_index_ref -> a_addr_ref (a_addrof l)
-  | L.Fun(f,l::p::_) when is_shiftable f -> a_shift (a_addrof l) p
+  | L.Fun(f,l::p::_) when is_shiftable f -> MemAddr.shift (a_addrof l) p
   | L.Fun(f,es) -> (IndexBuiltin.find f).addrof es
   | _ -> raise Not_found
 
@@ -160,9 +154,9 @@ let phi_consistent_range index sizeof =
 
 let () = Context.register
     begin fun () ->
-      MemMemory.register f_addr_var
+      MemAddr.register f_addr_var
         ~base:(F.e_fun f_base_var) ~offset:(fun _ -> F.e_zero) ;
-      MemMemory.register f_addr_ref
+      MemAddr.register f_addr_ref
         ~base:(F.e_fun f_base_ref) ;
       F.set_builtin_1 f_addrof phi_addrof ;
       F.set_builtin_1 f_consistent phi_consistent ;
@@ -252,7 +246,7 @@ struct
     | _ -> raise Not_found
 
   let builtin_addrof = function
-    | [l;p] -> a_shift (a_addrof l) p
+    | [l;p] -> MemAddr.shift (a_addrof l) p
     | _ -> raise Not_found
 
   let builtin_consistent fds = function
@@ -316,7 +310,7 @@ struct
   (* Address shift with coefficient c_i for each index k_i *)
   let rec shift a cs ks =
     match cs , ks with
-    | c::cs , k::ks -> shift (a_shift a (F.e_fact c k)) cs ks
+    | c::cs , k::ks -> shift (MemAddr.shift a (F.e_fact c k)) cs ks
     | _ -> a
 
   (* Address of an array index *)
@@ -785,7 +779,7 @@ struct
         let p = F.e_var xp in
         let a = to_addr loc in
         let n = F.e_int (Ctypes.bits_sizeof_object obj) in
-        let separated = p_separated p F.e_one a n in
+        let separated = F.p_call MemAddr.p_separated [ p ; F.e_one ; a ; n ] in
         let equal = F.p_equal (F.e_get m1 p) (F.e_get m2 p) in
         [xp],separated,equal
       else [],F.p_true,F.p_equal m1 m2
@@ -859,11 +853,11 @@ let sizeof = MODEL.sizeof
 
 let included s1 s2 =
   if disjoint_region s1 s2 then F.p_false else
-    MemMemory.included ~shift ~addrof ~sizeof s1 s2
+    MemAddr.included ~shift ~addrof ~sizeof s1 s2
 
 let separated s1 s2 =
   if disjoint_region s1 s2 then F.p_true else
-    MemMemory.separated ~shift ~addrof ~sizeof s1 s2
+    MemAddr.separated ~shift ~addrof ~sizeof s1 s2
 
 (* -------------------------------------------------------------------------- *)
 (* ---  TODO TODO TODO TODO TODO TODO TODO TODO TODO TODO TODO TODO TODO  --- *)
@@ -880,7 +874,7 @@ let apply _ _ = ()
 let literal ~eid _ = ignore eid ; GarbledMix
 
 let base_addr _l = GarbledMix
-let base_offset l = MemMemory.a_offset (addrof l)
+let base_offset l = MemAddr.offset (addrof l)
 let block_length _s _obj _l = F.e_zero
 
 let cast _ _l = GarbledMix
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index ad0596bfa8f081ac33f64782ef2fdbaa33143e12..24e7ddb49ea91e9ca78384e2b57770182557a1e0 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -45,8 +45,8 @@ let datatype = "MemTyped"
 let hypotheses p = p
 let configure () =
   begin
-    let orig_pointer = Context.push Lang.pointer t_addr in
-    let orig_null    = Context.push Cvalues.null (p_equal a_null) in
+    let orig_pointer = Context.push Lang.pointer MemAddr.t_addr in
+    let orig_null    = Context.push Cvalues.null (p_equal MemAddr.null) in
     let rollback () =
       Context.pop Lang.pointer orig_pointer ;
       Context.pop Cvalues.null orig_null ;
@@ -164,14 +164,14 @@ struct
     | M_int _ -> L.Int
     | M_f32 -> Cfloat.tau_of_float Ctypes.Float32
     | M_f64 -> Cfloat.tau_of_float Ctypes.Float64
-    | M_pointer -> t_addr
+    | M_pointer -> MemAddr.t_addr
     | T_alloc -> L.Int
     | T_init -> L.Bool
   let tau_of_chunk = function
-    | M_int _ -> 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)
+    | M_int _ -> L.Array(MemAddr.t_addr,L.Int)
+    | M_pointer -> L.Array(MemAddr.t_addr,MemAddr.t_addr)
+    | M_f32 -> L.Array(MemAddr.t_addr,Cfloat.tau_of_float Ctypes.Float32)
+    | M_f64 -> L.Array(MemAddr.t_addr,Cfloat.tau_of_float Ctypes.Float64)
     | T_alloc -> t_malloc
     | T_init -> t_init
   let basename_of_chunk = basename
@@ -302,15 +302,15 @@ type shift =
   | RS_Index of term  (* size of the shift *)
 
 let phi_base = function
-  | p::_ -> a_base p
+  | p::_ -> MemAddr.base p
   | _ -> raise Not_found
 
 let phi_field offset = function
-  | [p] -> e_add (a_offset p) offset
+  | [p] -> e_add (MemAddr.offset p) offset
   | _ -> raise Not_found
 
 let phi_index size = function
-  | [p;k] -> e_add (a_offset p) (F.e_mul size k)
+  | [p;k] -> e_add (MemAddr.offset p) (F.e_mul size k)
   | _ -> raise Not_found
 
 module RegisterShift = WpContext.Static
@@ -328,16 +328,16 @@ module ShiftFieldDef = WpContext.StaticGenerator(Cil_datatype.Fieldinfo)
       type data = dfun
 
       let generate f =
-        let result = t_addr in
+        let result = MemAddr.t_addr in
         let lfun = Lang.generated_f ~result "shiftfield_%s" (Lang.field_id f) in
         let position = position_of_field f in
         (* Since its a generated it is the unique name given *)
-        let xloc = Lang.freshvar ~basename:"p" t_addr in
+        let xloc = Lang.freshvar ~basename:"p" MemAddr.t_addr in
         let loc = e_var xloc in
-        let def = a_shift loc position in
+        let def = MemAddr.shift loc position in
         let dfun = Definitions.Function( result , Def , def) in
         RegisterShift.define lfun (RS_Field(f,position)) ;
-        MemMemory.register ~base:phi_base ~offset:(phi_field position) lfun ;
+        MemAddr.register ~base:phi_base ~offset:(phi_field position) lfun ;
         {
           d_lfun = lfun ; d_types = 0 ;
           d_params = [xloc] ;
@@ -389,18 +389,18 @@ module ShiftGen = WpContext.StaticGenerator(Cobj)
       let c_object_id c = Format.asprintf "%a@?" c_object_id c
 
       let generate obj =
-        let result = t_addr in
+        let result = MemAddr.t_addr in
         let shift = Lang.generated_f ~result "shift_%s" (c_object_id obj) in
         let size = length_of_object obj in
         (* Since its a generated it is the unique name given *)
-        let xloc = Lang.freshvar ~basename:"p" t_addr in
+        let xloc = Lang.freshvar ~basename:"p" MemAddr.t_addr in
         let loc = e_var xloc in
         let xk = Lang.freshvar ~basename:"k" Qed.Logic.Int in
         let k = e_var xk in
-        let def = a_shift loc (F.e_mul size k) in
+        let def = MemAddr.shift loc (F.e_mul size k) in
         let dfun = Definitions.Function( result , Def , def) in
         RegisterShift.define shift (RS_Index size) ;
-        MemMemory.register ~base:phi_base ~offset:(phi_index size)
+        MemAddr.register ~base:phi_base ~offset:(phi_index size)
           ~linear:true shift ;
         {
           d_lfun = shift ; d_types = 0 ;
@@ -455,7 +455,7 @@ module STRING = WpContext.Generator(LITERAL)
         let name = prefix ^ "_linked" in
         let a = Lang.freshvar ~basename:"alloc" (Chunk.tau_of_chunk T_alloc) in
         let m = e_var a in
-        let m_linked = p_call p_linked [m] in
+        let m_linked = MemAddr.linked m in
         let alloc = F.e_get m base in (* The size is alloc-1 *)
         let sized = Cstring.str_len cst (F.e_add alloc F.e_minus_one) in
         Definitions.define_lemma {
@@ -472,7 +472,7 @@ module STRING = WpContext.Generator(LITERAL)
         Definitions.define_lemma {
           l_kind = Admit ;
           l_name = name ; l_triggers = [] ; l_forall = [] ;
-          l_lemma = p_equal (e_fun f_region [base]) (e_int re) ;
+          l_lemma = p_equal (MemAddr.region base) (e_int re) ;
           l_cluster = Cstring.cluster () ;
         }
 
@@ -482,10 +482,10 @@ module STRING = WpContext.Generator(LITERAL)
         let i = Lang.freshvar ~basename:"i" L.Int in
         let c = Cstring.char_at cst (e_var i) in
         let ikind = Ctypes.c_char () in
-        let addr = shift (a_global base) (C_int ikind) (e_var i) in
+        let addr = shift (MemAddr.global base) (C_int ikind) (e_var i) in
         let m =
           Lang.freshvar ~basename:"mchar" (Chunk.tau_of_chunk (M_int ikind)) in
-        let m_sconst = F.p_call p_sconst [e_var m] in
+        let m_sconst = MemMemory.sconst (e_var m) in
         let v = F.e_get (e_var m) addr in
         let read = F.p_equal c v in
         Definitions.define_lemma {
@@ -549,7 +549,7 @@ module BASE = WpContext.Generator(Varinfo)
         Definitions.define_lemma {
           l_kind = Admit ;
           l_name = name ; l_triggers = [] ; l_forall = [] ;
-          l_lemma = p_equal (e_fun f_region [base]) (e_int re) ;
+          l_lemma = p_equal (MemAddr.region base) (e_int re) ;
           l_cluster = cluster_globals () ;
         }
 
@@ -568,7 +568,7 @@ module BASE = WpContext.Generator(Varinfo)
         | Some size ->
           let a = Lang.freshvar ~basename:"alloc" t_malloc in
           let m = e_var a in
-          let m_linked = p_call p_linked [m] in
+          let m_linked = MemAddr.linked m in
           let base_size = p_equal (F.e_get m base) size in
           Definitions.define_lemma {
             l_kind = Admit ;
@@ -585,11 +585,11 @@ module BASE = WpContext.Generator(Varinfo)
           let m = e_var a in
           let init_access =
             if size = e_one then
-              p_bool (F.e_get m (a_addr base e_zero))
+              p_bool (F.e_get m (MemAddr.mk_addr base e_zero))
             else
-              F.p_call p_is_init_r [ m ; a_addr base e_zero ; size ]
+              F.p_call p_is_init_r [ m ; MemAddr.mk_addr base e_zero ; size ]
           in
-          let m_init = p_call p_cinits [m] in
+          let m_init = MemMemory.cinits m in
           let init_prop = p_forall [a] (p_imply m_init init_access) in
           Definitions.define_lemma {
             l_kind = Admit ;
@@ -631,20 +631,20 @@ module BASE = WpContext.Generator(Varinfo)
 (* --- Locations                                                          --- *)
 (* -------------------------------------------------------------------------- *)
 
-let null = a_null (* as a loc *)
+let null = MemAddr.null (* as a loc *)
 
 let literal ~eid cst =
-  shift (a_global (STRING.get (eid,cst))) (C_int (Ctypes.c_char ())) e_zero
+  shift (MemAddr.global (STRING.get (eid,cst))) (C_int (Ctypes.c_char ())) e_zero
 
-let cvar x = a_global (BASE.get x)
+let cvar x = MemAddr.global (BASE.get x)
 
 let pointer_loc t = t
 let pointer_val t = t
 
-let allocated sigma l = F.e_get (Sigma.value sigma T_alloc) (a_base l)
+let allocated sigma l = F.e_get (Sigma.value sigma T_alloc) (MemAddr.base l)
 
-let base_addr l = a_addr (a_base l) e_zero
-let base_offset l = a_base_offset (a_base l) (a_offset l)
+let base_addr l = MemAddr.mk_addr (MemAddr.base l) e_zero
+let base_offset l = MemAddr.base_offset (MemAddr.base l) (MemAddr.offset l)
 let block_length sigma obj l =
   let n_cells = e_div (allocated sigma l) (length_of_object obj) in
   match obj with
@@ -954,8 +954,8 @@ let cast s l =
             "%a" pp_mismatch s ; l
     end
 
-let loc_of_int _ v = F.e_fun f_addr_of_int [v]
-let int_of_loc _ l = F.e_fun f_int_of_addr [l]
+let loc_of_int _ v = MemAddr.addr_of_int v
+let int_of_loc _ l = MemAddr.int_of_addr l
 
 (* -------------------------------------------------------------------------- *)
 (* --- Frames                                                             --- *)
@@ -1052,10 +1052,10 @@ struct
     F.p_call p_eqmem [m1;m2;loc;length_of_object obj]
 
   let eqmem_forall obj loc _chunk m1 m2 =
-    let xp = Lang.freshvar ~basename:"p" t_addr in
+    let xp = Lang.freshvar ~basename:"p" MemAddr.t_addr in
     let p = F.e_var xp in
     let n = length_of_object obj in
-    let separated = F.p_call p_separated [p;e_one;loc;n] in
+    let separated = F.p_call MemAddr.p_separated [p;e_one;loc;n] in
     let equal = p_equal (e_get m1 p) (e_get m2 p) in
     [xp],separated,equal
 
@@ -1096,7 +1096,7 @@ let domain = LOADER.domain
 
 let assigned seq obj loc =
   (* Maintain always initialized values initialized *)
-  Assert (p_call p_cinits [Sigma.value seq.post T_init]) ::
+  Assert (MemMemory.cinits (Sigma.value seq.post T_init)) ::
   LOADER.assigned seq obj loc
 
 (* -------------------------------------------------------------------------- *)
@@ -1104,17 +1104,17 @@ let assigned seq obj loc =
 (* -------------------------------------------------------------------------- *)
 
 let loc_compare f_cmp i_cmp p q =
-  match F.is_equal (a_base p) (a_base q) with
-  | L.Yes -> i_cmp (a_offset p) (a_offset q)
-  | L.Maybe | L.No -> p_call f_cmp [p;q]
+  match F.is_equal (MemAddr.base p) (MemAddr.base q) with
+  | L.Yes -> i_cmp (MemAddr.offset p) (MemAddr.offset q)
+  | L.Maybe | L.No -> f_cmp p q
 
 let is_null l = p_equal l null
 let loc_eq = p_equal
 let loc_neq = p_neq
-let loc_lt = loc_compare p_addr_lt p_lt
-let loc_leq = loc_compare p_addr_le p_leq
+let loc_lt = loc_compare MemAddr.addr_lt p_lt
+let loc_leq = loc_compare MemAddr.addr_le p_leq
 let loc_diff obj p q =
-  let delta = e_sub (a_offset p) (a_offset q) in
+  let delta = e_sub (MemAddr.offset p) (MemAddr.offset q) in
   let size = length_of_object obj in
   e_div delta size
 
@@ -1123,15 +1123,15 @@ let loc_diff obj p q =
 (* -------------------------------------------------------------------------- *)
 
 let s_valid sigma acs p n =
-  let p_valid = match acs with
-    | RW -> p_valid_rw
-    | RD -> p_valid_rd
-    | OBJ -> p_valid_obj
+  let valid = match acs with
+    | RW -> MemAddr.valid_rw
+    | RD -> MemAddr.valid_rd
+    | OBJ -> MemAddr.valid_obj
   in
-  p_call p_valid [Sigma.value sigma T_alloc;p;n]
+  valid (Sigma.value sigma T_alloc) p n
 
 let s_invalid sigma p n =
-  p_call p_invalid [Sigma.value sigma T_alloc;p;n]
+  MemAddr.invalid (Sigma.value sigma T_alloc) p n
 
 let segment phi = function
   | Rloc(obj,l) ->
@@ -1151,13 +1151,13 @@ let invalid sigma = segment (s_invalid sigma)
 let frame sigma =
   let wellformed_frame phi chunk =
     if Sigma.mem sigma chunk
-    then [ p_call phi [Sigma.value sigma chunk] ]
+    then [ phi (Sigma.value sigma chunk) ]
     else []
   in
-  wellformed_frame p_linked T_alloc @
-  wellformed_frame p_cinits T_init @
-  wellformed_frame p_sconst (M_int (Ctypes.c_char ())) @
-  wellformed_frame p_framed M_pointer
+  wellformed_frame MemAddr.linked T_alloc @
+  wellformed_frame MemMemory.cinits T_init @
+  wellformed_frame MemMemory.sconst (M_int (Ctypes.c_char ())) @
+  wellformed_frame MemMemory.framed M_pointer
 
 let alloc sigma xs =
   if xs = [] then sigma else Sigma.havoc_chunk sigma T_alloc
@@ -1174,7 +1174,7 @@ let scope seq scope xs =
         (Sigma.value seq.pre T_alloc) xs in
     [ p_equal (Sigma.value seq.post T_alloc) alloc ]
 
-let global _sigma p = p_leq (e_fun f_region [a_base p]) e_zero
+let global _sigma p = p_leq MemAddr.(region @@ base p) e_zero
 
 (* -------------------------------------------------------------------------- *)
 (* --- Segments                                                           --- *)
@@ -1183,12 +1183,12 @@ let global _sigma p = p_leq (e_fun f_region [a_base p]) e_zero
 let included =
   let addrof l = l in
   let sizeof = length_of_object in
-  MemMemory.included ~shift ~addrof ~sizeof
+  MemAddr.included ~shift ~addrof ~sizeof
 
 let separated =
   let addrof l = l in
   let sizeof = length_of_object in
-  MemMemory.separated ~shift ~addrof ~sizeof
+  MemAddr.separated ~shift ~addrof ~sizeof
 
 (* -------------------------------------------------------------------------- *)
 (* --- State Model                                                        --- *)
@@ -1198,7 +1198,7 @@ type state = chunk Tmap.t
 
 let rec lookup_a e =
   match F.repr e with
-  | L.Fun( f , [e] ) when f == f_global -> lookup_a e
+  | L.Fun( f , [e] ) when MemAddr.is_f_global f -> lookup_a e
   | L.Fun( f , es ) -> lookup_f f es
   | _ -> raise Not_found
 
diff --git a/src/plugins/wp/TacHavoc.ml b/src/plugins/wp/TacHavoc.ml
index 412c49592ae8c9f2ff585d46d69f49c4f714c85f..87cb011e34ce10ee3f8ed8426f1382dfced06449 100644
--- a/src/plugins/wp/TacHavoc.ml
+++ b/src/plugins/wp/TacHavoc.ml
@@ -55,7 +55,7 @@ class havoc =
       | None -> Not_applicable
       | Some(mr,m0,a,n,p) ->
         let separated =
-          F.p_call MemMemory.p_separated
+          F.p_call MemAddr.p_separated
             [ p ; F.e_int 1 ; a ; n ] in
         let process = Tactical.rewrite ?at [
             "Unassigned" , separated , e , F.e_get m0 p ;
@@ -70,11 +70,11 @@ class havoc =
 
 let separated ?at property =
   match F.e_expr property with
-  | L.Fun( f , [p;n;q;m] ) when f == MemMemory.p_separated ->
-    let base_p = MemMemory.a_base p in
-    let ofs_p = MemMemory.a_offset p in
-    let base_q = MemMemory.a_base q in
-    let ofs_q = MemMemory.a_offset q in
+  | L.Fun( f , [p;n;q;m] ) when f == MemAddr.p_separated ->
+    let base_p = MemAddr.base p in
+    let ofs_p = MemAddr.offset p in
+    let base_q = MemAddr.base q in
+    let ofs_q = MemAddr.offset q in
     let eq_base = F.p_equal base_p base_q in
     let on_left = F.p_leq (F.e_add ofs_p n) ofs_q in
     let on_right = F.p_leq (F.e_add ofs_q m) ofs_p in
@@ -110,8 +110,8 @@ class separated =
 (* -------------------------------------------------------------------------- *)
 
 let invalid m p n =
-  let base = MemMemory.a_base p in
-  let offset = MemMemory.a_offset p in
+  let base = MemAddr.base p in
+  let offset = MemAddr.offset p in
   let malloc = F.e_get m base in
   "Invalid",
   F.p_imply
@@ -121,8 +121,8 @@ let invalid m p n =
        (F.p_leq (F.e_add offset n) F.e_zero))
 
 let valid_rd m p n =
-  let base = MemMemory.a_base p in
-  let offset = MemMemory.a_offset p in
+  let base = MemAddr.base p in
+  let offset = MemAddr.offset p in
   let malloc = F.e_get m base in
   "Valid (Read)",
   F.p_imply
@@ -132,8 +132,8 @@ let valid_rd m p n =
        (F.p_leq (F.e_add offset n) malloc))
 
 let valid_rw m p n =
-  let base = MemMemory.a_base p in
-  let offset = MemMemory.a_offset p in
+  let base = MemAddr.base p in
+  let offset = MemAddr.offset p in
   let malloc = F.e_get m base in
   "Valid (Read & Write)",
   F.p_imply
@@ -145,10 +145,10 @@ let valid_rw m p n =
       ])
 
 let included p a q b =
-  let p_base = MemMemory.a_base p in
-  let q_base = MemMemory.a_base q in
-  let p_offset = MemMemory.a_offset p in
-  let q_offset = MemMemory.a_offset q in
+  let p_base = MemAddr.base p in
+  let q_base = MemAddr.base q in
+  let p_offset = MemAddr.offset p in
+  let q_offset = MemAddr.offset q in
   "Included",
   F.p_imply
     (F.p_lt F.e_zero a)
@@ -161,10 +161,10 @@ let included p a q b =
          ]))
 
 let lookup f = function
-  | [p;a;q;b] when f == MemMemory.p_included -> included p a q b
-  | [m;p;n] when f == MemMemory.p_invalid -> invalid m p n
-  | [m;p;n] when f == MemMemory.p_valid_rd -> valid_rd m p n
-  | [m;p;n] when f == MemMemory.p_valid_rw -> valid_rw m p n
+  | [p;a;q;b] when f == MemAddr.p_included -> included p a q b
+  | [m;p;n] when MemAddr.is_p_invalid f -> invalid m p n
+  | [m;p;n] when MemAddr.is_p_valid_rd f -> valid_rd m p n
+  | [m;p;n] when MemAddr.is_p_valid_rw f -> valid_rw m p n
   | _ -> raise Not_found
 
 let unfold ?at e f es =
diff --git a/src/plugins/wp/dune b/src/plugins/wp/dune
index ec906197b6dd444a081afebd27ca36de2600d6ab..1e53b4d17b0373062e0141cb5ca849d1d679a501 100644
--- a/src/plugins/wp/dune
+++ b/src/plugins/wp/dune
@@ -61,6 +61,7 @@
     (share/why3/frama_c_wp/cint.mlw as wp/why3/frama_c_wp/cint.mlw)
     (share/why3/frama_c_wp/qed.mlw as wp/why3/frama_c_wp/qed.mlw)
     (share/why3/frama_c_wp/vset.mlw as wp/why3/frama_c_wp/vset.mlw)
+    (share/why3/frama_c_wp/memaddr.mlw as wp/why3/frama_c_wp/memaddr.mlw)
     (share/why3/frama_c_wp/memory.mlw as wp/why3/frama_c_wp/memory.mlw)
     (share/why3/frama_c_wp/cmath.mlw as wp/why3/frama_c_wp/cmath.mlw)
     (share/why3/frama_c_wp/cfloat.mlw as wp/why3/frama_c_wp/cfloat.mlw)
diff --git a/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw b/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..3dda4f82d376a5cb1b77a644d0567910a8ee8daa
--- /dev/null
+++ b/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
@@ -0,0 +1,162 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of WP plug-in of Frama-C.                           *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2023                                               *)
+(*    CEA (Commissariat a l'energie atomique et aux energies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+theory MemAddr
+
+  use bool.Bool
+  use int.Int
+  use map.Map
+
+  type addr = { base : int ; offset : int }
+  type malloc = map int int
+
+  (* Special addresses *)
+
+  constant null: addr = { base = 0 ; offset = 0 }
+  function global (b: int) : addr = { base = b ; offset = 0 }
+  meta "inline:no" function null
+  meta "inline:no" function global
+
+  (* Pointer arithmetic *)
+
+  predicate addr_le addr addr
+  predicate addr_lt addr addr
+  function addr_le_bool addr addr : bool
+  function addr_lt_bool addr addr : bool
+
+  axiom addr_le_def:
+    forall p q: addr [addr_le p q].
+      p.base = q.base -> (addr_le p q <-> p.offset <= q.offset)
+
+  axiom addr_lt_def:
+    forall p q: addr [addr_lt p q].
+      p.base = q.base -> (addr_lt p q <-> p.offset < q.offset)
+
+  axiom addr_le_bool_def:
+    forall p q: addr [ addr_le_bool p q].
+      addr_le p q <-> addr_le_bool p q = True
+
+  axiom addr_lt_bool_def:
+    forall p q: addr [ addr_lt_bool p q].
+      addr_lt p q <-> addr_lt_bool p q = True
+
+
+  function shift (p: addr) (k: int) : addr = { p with offset = p.offset + k }
+
+  (* Validity *)
+
+  predicate valid_rw (m: malloc) (p: addr) (n: int) =
+    n > 0 -> (  0 < p.base /\ 0 <= p.offset /\ p.offset + n <= m[p.base] )
+
+  predicate valid_rd (m: malloc) (p: addr) (n: int) =
+    n > 0 -> ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= m[p.base] )
+
+  predicate valid_obj (m: malloc) (p: addr) (n: int) =
+    n > 0 -> ( p = null \/
+             ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= 1 + m[p.base] ))
+
+  predicate invalid (m : malloc) (p:addr) (n:int) =
+    n <= 0 \/ p.base = 0 \/ m[p.base] <= p.offset \/ p.offset + n <= 0
+
+  lemma valid_rw_rd:
+    forall m: malloc. forall p: addr. forall n: int.
+      valid_rw m p n -> valid_rd m p n
+
+  lemma valid_string:
+    forall m: malloc. forall p: addr.
+      p.base < 0 -> 0 <= p.offset < m[p.base] ->
+        (valid_rd m p 1 /\ not (valid_rw m p 1))
+
+  (* Separation and inclusion *)
+
+  predicate included (p: addr) (lp: int) (q: addr) (lq: int) =
+    lp > 0 -> ( lq >= 0 /\ p.base = q.base
+                      /\ (q.offset <= p.offset)
+                      /\ (p.offset + lp <= q.offset + lq) )
+
+  predicate separated (p: addr) (lp: int) (q: addr) (lq: int) =
+       lp <= 0 \/ lq <= 0
+    \/ p.base <> q.base
+    \/ q.offset + lq <= p.offset
+    \/ p.offset + lp <= q.offset
+
+  lemma separated_1:
+    forall p q: addr. forall lp lq i j: int
+      [ separated p lp q lq , { base = p.base ; offset = i } ,
+                              { base = q.base ; offset = j } ].
+      separated p lp q lq ->
+      p.offset <= i < p.offset + lp ->
+      q.offset <= j < q.offset + lq ->
+        { base = p.base ; offset = i } <>
+        { base = q.base ; offset = j }
+
+  lemma separated_included:
+    forall p q: addr. forall lp lq: int
+      [ separated p lp q lq , included p lp q lq ].
+      lp > 0 -> lq > 0 -> separated p lp q lq -> included p lp q lq -> false
+
+  lemma included_trans:
+    forall p q r: addr. forall lp lq lr: int
+      [ included p lp q lq , included q lq r lr ].
+    included p lp q lq -> included q lq r lr -> included p lp r lr
+
+  lemma separated_trans:
+    forall p q r: addr. forall lp lq lr : int
+      [ included p lp q lq , separated q lq r lr ].
+    included p lp q lq -> separated q lq r lr -> separated p lp r lr
+
+  lemma separated_sym:
+    forall p q : addr. forall lp lq : int
+      [ separated p lp q lq ].
+      separated p lp q lq <-> separated q lq p lp
+
+  (* Regions *)
+
+  function region int: int
+  predicate linked (malloc)
+
+  (* Physical Address *)
+
+  function int_of_addr addr: int
+  function addr_of_int int: addr
+
+  type table (* abstract for now, but can be more elaborated later on *)
+  function table_of_base int: table
+  function table_to_offset table int: int
+
+  axiom table_to_offset_zero:
+    forall t: table. table_to_offset t 0 = 0
+
+  axiom table_to_offset_monotonic:
+    forall t: table. forall o1 o2: int.
+      o1 <= o2 <-> table_to_offset t o1 <= table_to_offset t o2
+
+  axiom int_of_addr_bijection :
+    forall a:int. int_of_addr (addr_of_int a) = a
+
+  axiom addr_of_int_bijection :
+    forall p:addr. addr_of_int (int_of_addr p) = p
+
+  axiom addr_of_null :
+    int_of_addr null = 0
+
+end
diff --git a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
index d153801e34018a2125080d254a25660d634b323a..df3bc8578965be946d9f1c941ac757c851df3412 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
@@ -25,119 +25,18 @@ theory Memory
   use bool.Bool
   use int.Int
   use map.Map
-
-  type addr = { base : int ; offset : int }
-
-  predicate addr_le addr addr
-  predicate addr_lt addr addr
-  function addr_le_bool addr addr : bool
-  function addr_lt_bool addr addr : bool
-
-  axiom addr_le_def: forall p q :addr [addr_le p q].
-    p.base = q.base -> (addr_le p q <-> p.offset <= q.offset)
-
-  axiom addr_lt_def: forall p q :addr [addr_lt p q].
-    p.base = q.base -> (addr_lt p q <-> p.offset < q.offset)
-
-  axiom addr_le_bool_def : forall p q : addr [ addr_le_bool p q].
-    addr_le p q <-> addr_le_bool p q = True
-
-  axiom addr_lt_bool_def : forall p q : addr [ addr_lt_bool p q].
-    addr_lt p q <-> addr_lt_bool p q = True
-
-  constant null : addr = { base = 0 ; offset = 0 }
-  function global (b:int) : addr = { base = b ; offset = 0 }
-  meta "inline:no" function null
-  meta "inline:no" function global
-
-  function shift (p:addr) (k:int) : addr = { p with offset = p.offset + k }
-  predicate included (p:addr) (a:int) (q:addr) (b:int) =
-    a > 0 -> ( b >= 0 /\ p.base = q.base
-                     /\ (q.offset <= p.offset)
-                     /\ (p.offset + a <= q.offset + b) )
-
-  predicate separated (p:addr) (a:int) (q:addr) (b:int) =
-       a <= 0 \/ b <= 0
-    \/ p.base <> q.base
-    \/ q.offset + b <= p.offset
-    \/ p.offset + a <= q.offset
+  use frama_c_wp.memaddr.MemAddr
 
   (* Memories *)
 
-  predicate eqmem (m1 m2 : map addr 'a) (p:addr) (a:int) =
-    forall q:addr [m1[p]|m2[q]]. included q 1 p a -> m1[q] = m2[q]
-
-  function havoc (m0 m1 : map addr 'a) (p:addr) (a:int) : map addr 'a
-
-  predicate valid_rw (m : map int int) (p:addr) (n:int) =
-    n > 0 -> (  0 < p.base /\ 0 <= p.offset /\ p.offset + n <= m[p.base] )
-
-  predicate valid_rd (m : map int int) (p:addr) (n:int) =
-    n > 0 -> ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= m[p.base] )
-
-  predicate valid_obj (m : map int int) (p:addr) (n:int) =
-    n > 0 -> ( p = null \/
-             ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= 1 + m[p.base] ))
-
-  predicate invalid (m : map int int) (p:addr) (n:int) =
-    n <= 0 \/ p.base = 0 \/ m[p.base] <= p.offset \/ p.offset + n <= 0
-
-  lemma valid_rw_rd :
-    forall m : map int int.
-    forall p : addr.
-    forall n : int.
-    valid_rw m p n -> valid_rd m p n
-
-  lemma valid_string :
-    forall m : map int int.
-    forall p : addr.
-    p.base < 0 ->
-    0 <= p.offset < m[p.base] ->
-    (valid_rd m p 1 /\ not (valid_rw m p 1))
-
-  lemma separated_1 : forall p q : addr. forall a b i j : int
-    [ separated p a q b , { base = p.base ; offset = i } ,
-                          { base = q.base ; offset = j } ].
-    separated p a q b ->
-    p.offset <= i < p.offset + a ->
-    q.offset <= j < q.offset + b ->
-    { base = p.base ; offset = i } <>
-    { base = q.base ; offset = j }
-
-  (* Regions *)
-
-  function region int : int
-
-  predicate linked (map int int)
   predicate sconst (map addr int)
   predicate framed (m : map addr addr) =
     forall p:addr [m[p]]. region(p.base) <= 0 -> region(m[p].base) <= 0
 
-  (* Properties *)
+  predicate eqmem (m1 m2 : map addr 'a) (p:addr) (a:int) =
+    forall q:addr [m1[p]|m2[q]]. included q 1 p a -> m1[q] = m2[q]
 
-  lemma separated_included :
-    forall p q : addr.
-    forall a b : int
-      [ separated p a q b , included p a q b ].
-    a > 0 -> b > 0 -> separated p a q b -> included p a q b -> false
-
-  lemma included_trans :
-    forall p q r : addr.
-    forall a b c : int
-      [ included p a q b , included q b r c ].
-    included p a q b -> included q b r c -> included p a r c
-
-  lemma separated_trans :
-    forall p q r : addr.
-    forall a b c : int
-      [ included p a q b , separated q b r c ].
-    included p a q b -> separated q b r c -> separated p a r c
-
-  lemma separated_sym :
-    forall p q : addr.
-    forall a b : int
-      [ separated p a q b ].
-    separated p a q b <-> separated q b p a
+  function havoc (m0 m1 : map addr 'a) (p:addr) (a:int) : map addr 'a
 
   lemma eqmem_included :
     forall m1 m2 : map addr 'a.
@@ -178,29 +77,4 @@ theory Memory
   predicate monotonic_init(m1 m2 : map addr bool) =
     forall p: addr. m1[p] -> m2[p]
 
-  (* Physical Address *)
-
-  function int_of_addr addr : int
-  function addr_of_int int : addr
-
-  type table (* abstract for now, but can be more elaborated later on *)
-  function table_of_base int : table
-  function table_to_offset table int : int
-
-  axiom table_to_offset_zero:
-    forall t: table. table_to_offset t 0 = 0
-
-  axiom table_to_offset_monotonic:
-    forall t: table. forall o1 o2: int.
-      o1 <= o2 <-> table_to_offset t o1 <= table_to_offset t o2
-
-  axiom int_of_addr_bijection :
-    forall a:int. int_of_addr (addr_of_int a) = a
-
-  axiom addr_of_int_bijection :
-    forall p:addr. addr_of_int (int_of_addr p) = p
-
-  axiom addr_of_null :
-    int_of_addr null = 0
-
 end
diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver
index 7f473abbea88e3f73f84ac6b41db8fcdef5edb0c..52b3e021364caa844726656f22dcfb89ca2b5d6d 100644
--- a/src/plugins/wp/share/wp.driver
+++ b/src/plugins/wp/share/wp.driver
@@ -86,7 +86,10 @@ why3.import := "vset.Vset";
 library vlist:
 why3.import := "frama_c_wp.vlist.Vlist";
 
-library memory:
+library memaddr:
+why3.import := "frama_c_wp.memaddr.MemAddr";
+
+library memory: memaddr
 why3.import := "frama_c_wp.memory.Memory";
 
 library sqrt: cmath
diff --git a/src/plugins/wp/tests/why3/spec_memory.why b/src/plugins/wp/tests/why3/spec_memory.why
index 6c1f84a465e774c3f2ce7d0961d4a9e8a9968f0e..29d0887963627a29b9eb99bfac31337249e89fe4 100644
--- a/src/plugins/wp/tests/why3/spec_memory.why
+++ b/src/plugins/wp/tests/why3/spec_memory.why
@@ -3,7 +3,7 @@ module Spec_memory
   use int.Int
   use map.Map
 
-  use frama_c_wp.memory.Memory
+  use frama_c_wp.memaddr.MemAddr
 
   type malloc = map int int
 
diff --git a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
index bba94a31d5f562ce29b573eb64d0ee7dc5ffd21e..a415fcd4524da1e46c9fdb0aff4321a269627293 100644
--- a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
@@ -23,7 +23,7 @@ theory Compound
   
   (* use map.Map *)
   
-  (* use frama_c_wp.memory.Memory *)
+  (* use frama_c_wp.memaddr.MemAddr *)
   
   function shift_sint32 (p:addr) (k:int) : addr = shift p k
 end
@@ -43,7 +43,7 @@ end
     
     (* use map.Map *)
     
-    (* use frama_c_wp.memory.Memory *)
+    (* use frama_c_wp.memaddr.MemAddr *)
     
     (* use frama_c_wp.cint.Cint *)
     
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
index 6514809aaf78a858612e4af77acd5b5a9c5e589f..a52cc11028400374f3a3ca8a9ecd1f8a43e6127f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
@@ -26,7 +26,7 @@ theory Chunk
   
   (* use map.Map *)
   
-  (* use frama_c_wp.memory.Memory *)
+  (* use frama_c_wp.memaddr.MemAddr *)
   
   (* use frama_c_wp.cint.Cint *)
   
@@ -51,7 +51,7 @@ theory Compound
   
   (* use map.Map *)
   
-  (* use frama_c_wp.memory.Memory *)
+  (* use frama_c_wp.memaddr.MemAddr *)
   
   function shift_sint32 (p:addr) (k:int) : addr = shift p k
 end
@@ -73,7 +73,7 @@ theory A_Occ
   
   (* use map.Map *)
   
-  (* use frama_c_wp.memory.Memory *)
+  (* use frama_c_wp.memaddr.MemAddr *)
   
   function L_occ (addr -> int) int addr int int : int
   
@@ -122,7 +122,7 @@ theory Axiomatic1
   
   (* use map.Map *)
   
-  (* use frama_c_wp.memory.Memory *)
+  (* use frama_c_wp.memaddr.MemAddr *)
   
   (* use Chunk *)
   
@@ -184,7 +184,7 @@ theory Chunk1
   
   (* use map.Map1 *)
   
-  (* use frama_c_wp.memory.Memory1 *)
+  (* use frama_c_wp.memaddr.MemAddr1 *)
   
   (* use frama_c_wp.cint.Cint1 *)
   
@@ -209,7 +209,7 @@ theory Compound1
   
   (* use map.Map1 *)
   
-  (* use frama_c_wp.memory.Memory1 *)
+  (* use frama_c_wp.memaddr.MemAddr1 *)
   
   function shift_sint321 (p:addr1) (k:int) : addr1 = shift1 p k
 end
@@ -231,7 +231,7 @@ theory A_Occ1
   
   (* use map.Map1 *)
   
-  (* use frama_c_wp.memory.Memory1 *)
+  (* use frama_c_wp.memaddr.MemAddr1 *)
   
   function L_occ1 (addr1 -> int) int addr1 int int : int
   
@@ -282,7 +282,7 @@ theory Axiomatic11
   
   (* use map.Map1 *)
   
-  (* use frama_c_wp.memory.Memory1 *)
+  (* use frama_c_wp.memaddr.MemAddr1 *)
   
   (* use Chunk1 *)
   
@@ -343,7 +343,7 @@ theory Chunk2
   
   (* use map.Map2 *)
   
-  (* use frama_c_wp.memory.Memory2 *)
+  (* use frama_c_wp.memaddr.MemAddr2 *)
   
   (* use frama_c_wp.cint.Cint2 *)
   
@@ -368,7 +368,7 @@ theory Compound2
   
   (* use map.Map2 *)
   
-  (* use frama_c_wp.memory.Memory2 *)
+  (* use frama_c_wp.memaddr.MemAddr2 *)
   
   function shift_sint322 (p:addr2) (k:int) : addr2 = shift2 p k
 end
@@ -390,7 +390,7 @@ theory A_Occ2
   
   (* use map.Map2 *)
   
-  (* use frama_c_wp.memory.Memory2 *)
+  (* use frama_c_wp.memaddr.MemAddr2 *)
   
   function L_occ2 (addr2 -> int) int addr2 int int : int
   
@@ -439,7 +439,7 @@ end
     
     (* use map.Map2 *)
     
-    (* use frama_c_wp.memory.Memory2 *)
+    (* use frama_c_wp.memaddr.MemAddr2 *)
     
     (* use Chunk2 *)
     
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
index 444fa41e01aa69044058c14920ddfa7f6441712c..fc53f6bcec0761474f5d95ba675a15b3c971e1f2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
@@ -20,7 +20,7 @@ theory Compound
   
   (* use map.Map *)
   
-  (* use frama_c_wp.memory.Memory *)
+  (* use frama_c_wp.memaddr.MemAddr *)
   
   function shift_sint32 (p:addr) (k:int) : addr = shift p k
   
@@ -50,7 +50,7 @@ end
     lemma Q_test_no_label :
       forall a:int, b:int, d:int. P_is_gcd a b d -> not P_is_gcd b d a
     
-    (* use frama_c_wp.memory.Memory *)
+    (* use frama_c_wp.memaddr.MemAddr *)
     
     (* use Compound *)
     
@@ -109,7 +109,7 @@ end
     
     (* use map.Map *)
     
-    (* use frama_c_wp.memory.Memory *)
+    (* use frama_c_wp.memaddr.MemAddr *)
     
     (* use Compound *)
     
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
index df6d4ce29fa743818fa496481c04b1901f967cef..0ffa139bbf1021b1267d76be1dd7466b7a0989e1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
@@ -23,7 +23,7 @@ theory Chunk
   
   (* use map.Map *)
   
-  (* use frama_c_wp.memory.Memory *)
+  (* use frama_c_wp.memaddr.MemAddr *)
   
   (* use frama_c_wp.cint.Cint *)
   
@@ -101,7 +101,7 @@ theory Compound
   
   (* use map.Map *)
   
-  (* use frama_c_wp.memory.Memory *)
+  (* use frama_c_wp.memaddr.MemAddr *)
   
   function shiftfield_F1_X_a (p:addr) : addr = shift p 0
   
@@ -128,6 +128,8 @@ theory Compound
      separated p 3 q 1 ->
      Load_S1_X p (set mchar q v) mint mint1 = Load_S1_X p mchar mint mint1
   
+  (* use frama_c_wp.memory.Memory *)
+  
   axiom Q_Load_S1_X_eqmem_Mchar0 :
     forall mchar:addr -> int, mchar1:addr -> int, mint:addr -> int, mint1:
      addr -> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint mint1,
@@ -226,10 +228,12 @@ end
     
     (* use map.Map *)
     
-    (* use frama_c_wp.memory.Memory *)
+    (* use frama_c_wp.memaddr.MemAddr *)
     
     (* use Chunk *)
     
+    (* use frama_c_wp.memory.Memory *)
+    
     (* use S1_X *)
     
     (* use Compound *)
@@ -262,12 +266,14 @@ end
     
     (* use map.Map *)
     
-    (* use frama_c_wp.memory.Memory *)
+    (* use frama_c_wp.memaddr.MemAddr *)
     
     (* use S1_X *)
     
     (* use Chunk *)
     
+    (* use frama_c_wp.memory.Memory *)
+    
     (* use Compound *)
     
     goal wp_goal :
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.2.res.oracle
index 3ad47363a3d0d1f8b1322d46a972f1886968ca8d..4dd7571870e8792ccb83e5393c72d9938a506a54 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.2.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.2.res.oracle
@@ -21,7 +21,7 @@ theory Axiomatic1
   
   (* use map.Map *)
   
-  (* use frama_c_wp.memory.Memory *)
+  (* use frama_c_wp.memaddr.MemAddr *)
   
   function L_x (mint:addr -> int) (p:addr) : int = get mint p
 end
@@ -41,7 +41,7 @@ end
     
     (* use map.Map *)
     
-    (* use frama_c_wp.memory.Memory *)
+    (* use frama_c_wp.memaddr.MemAddr *)
     
     (* use Axiomatic1 *)
     
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle
index bb22d8bc45b0a108885ac01f90e3d684eb08e177..e5be0ef4afa81eb38f9e905b856536f5163e4a97 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts0843.res.oracle
@@ -39,7 +39,7 @@ Let a = Mptr_0[global(G_p_20)].
 Let a_1 = shiftfield_F1_a(a).
 Assume {
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Goal *)
   When: !invalid(Malloc_0, a_1, 1).
   (* Pre-condition *)
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
index b0b18afa3218d25c649b9d732df7428e85813d1a..9b86f82b147c87916da165d370fad7fdd4e03c39 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
@@ -52,7 +52,7 @@ theory Compound
   
   (* use map.Map *)
   
-  (* use frama_c_wp.memory.Memory *)
+  (* use frama_c_wp.memaddr.MemAddr *)
   
   function shiftfield_F2_A_dummy (p:addr) : addr = shift p 0
   
@@ -68,6 +68,8 @@ theory Compound
      [Load_S2_A p (set mint q v)].
      not q = p -> Load_S2_A p (set mint q v) = Load_S2_A p mint
   
+  (* use frama_c_wp.memory.Memory *)
+  
   axiom Q_Load_S2_A_eqmem_Mint0 :
     forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
      [Load_S2_A p mint, eqmem mint mint1 q n| Load_S2_A p mint1,
@@ -97,7 +99,7 @@ end
     
     (* use map.Map *)
     
-    (* use frama_c_wp.memory.Memory *)
+    (* use frama_c_wp.memaddr.MemAddr *)
     
     (* use Compound *)
     
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
index e0b3a051e4e52ab6befe04639843d2ae5f3145d7..8705b618e28ca7a93f722e6f65d12d3bcc2502f2 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
@@ -20,7 +20,7 @@ theory Compound
   
   (* use map.Map *)
   
-  (* use frama_c_wp.memory.Memory *)
+  (* use frama_c_wp.memaddr.MemAddr *)
   
   function shift_sint32 (p:addr) (k:int) : addr = shift p k
   
@@ -42,7 +42,7 @@ end
     
     (* use map.Map *)
     
-    (* use frama_c_wp.memory.Memory *)
+    (* use frama_c_wp.memaddr.MemAddr *)
     
     (* use Compound *)
     
@@ -79,7 +79,7 @@ end
     
     (* use map.Map *)
     
-    (* use frama_c_wp.memory.Memory *)
+    (* use frama_c_wp.memaddr.MemAddr *)
     
     (* use Compound *)
     
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
index 7db02668070e5454af37cffbff04a5556d0a7d9f..ee9bc1e90ab5a193c0b57242c70778df7de94e3a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
@@ -25,7 +25,7 @@ theory Compound
   
   (* use map.Map *)
   
-  (* use frama_c_wp.memory.Memory *)
+  (* use frama_c_wp.memaddr.MemAddr *)
   
   function shift_sint32 (p:addr) (k:int) : addr = shift p k
 end
@@ -65,7 +65,7 @@ end
     
     (* use map.Map *)
     
-    (* use frama_c_wp.memory.Memory *)
+    (* use frama_c_wp.memaddr.MemAddr *)
     
     (* use frama_c_wp.cint.Cint *)
     
@@ -114,7 +114,7 @@ theory Compound1
   
   (* use map.Map1 *)
   
-  (* use frama_c_wp.memory.Memory1 *)
+  (* use frama_c_wp.memaddr.MemAddr1 *)
   
   function shift_sint321 (p:addr1) (k:int) : addr1 = shift1 p k
 end
@@ -154,7 +154,7 @@ end
     
     (* use map.Map1 *)
     
-    (* use frama_c_wp.memory.Memory1 *)
+    (* use frama_c_wp.memaddr.MemAddr1 *)
     
     (* use frama_c_wp.cint.Cint1 *)
     
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
index 3a316233827c1609d8a4c72c8c96bb4c614205db..5e41d21fadff5991d7d2c0b6eec7fdefe0a3d6e6 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
@@ -25,7 +25,7 @@ theory Compound
   
   (* use map.Map *)
   
-  (* use frama_c_wp.memory.Memory *)
+  (* use frama_c_wp.memaddr.MemAddr *)
   
   function shift_sint32 (p:addr) (k:int) : addr = shift p k
 end
@@ -65,7 +65,7 @@ end
     
     (* use map.Map *)
     
-    (* use frama_c_wp.memory.Memory *)
+    (* use frama_c_wp.memaddr.MemAddr *)
     
     (* use frama_c_wp.cint.Cint *)
     
@@ -108,7 +108,7 @@ theory Compound1
   
   (* use map.Map1 *)
   
-  (* use frama_c_wp.memory.Memory1 *)
+  (* use frama_c_wp.memaddr.MemAddr1 *)
   
   function shift_sint321 (p:addr1) (k:int) : addr1 = shift1 p k
 end
@@ -148,7 +148,7 @@ end
     
     (* use map.Map1 *)
     
-    (* use frama_c_wp.memory.Memory1 *)
+    (* use frama_c_wp.memaddr.MemAddr1 *)
     
     (* use frama_c_wp.cint.Cint1 *)
     
diff --git a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle
index 276a519cb4af75159523a97ca1a56b148dbfa76e..3220f8249fa637918bb762119c9d617002cc6cc3 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle
@@ -265,7 +265,7 @@ Goal Assertion (file array_initialized.c, line 283):
 Let a = global(K_p_34).
 Assume {
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Goal *)
   When: (0 <= i) /\ (i <= 499).
   (* Initializer *)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle
index 3304372daa264226c76184055f11cf12ac33341f..b9c15212aa337d0ee7c40a55c780bff68098d014 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle
@@ -52,7 +52,7 @@ Goal Assertion 'A,X' (file frame.i, line 34):
 Let a = Mptr_0[global(L_x_37)].
 Assume {
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Initializer *)
   Init: a = shiftfield_F2_S_b(global(P_s_36)).
 }
@@ -64,7 +64,7 @@ Goal Assertion 'A,Y' (file frame.i, line 35):
 Let a = Mptr_0[global(L_x_37)].
 Assume {
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Initializer *)
   Init: a = shiftfield_F2_S_b(global(P_s_36)).
   (* Assertion 'A,X' *)
@@ -81,7 +81,7 @@ Goal Assertion 'A,X' (file frame.i, line 25):
 Let a = Mptr_0[global(L_x_32)].
 Assume {
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Initializer *)
   Init: a = shift_sint8(global(L_b_31), 0).
 }
@@ -93,7 +93,7 @@ Goal Assertion 'A,Y' (file frame.i, line 26):
 Let a = Mptr_0[global(L_x_32)].
 Assume {
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Initializer *)
   Init: a = shift_sint8(global(L_b_31), 0).
   (* Assertion 'A,X' *)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle
index 8b0ea16e32ef953268d9cac73ff69b01f1dd07a3..2e3d693fe257f10d9efed06a58e2506ff85a88e4 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle
@@ -52,7 +52,7 @@ Goal Assertion 'A,X' (file frame.i, line 34):
 Let a = Mptr_0[global(L_x_37)].
 Assume {
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Initializer *)
   Init: a = shiftfield_F2_S_b(global(P_s_36)).
 }
@@ -64,7 +64,7 @@ Goal Assertion 'A,Y' (file frame.i, line 35):
 Let a = Mptr_0[global(L_x_37)].
 Assume {
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Initializer *)
   Init: a = shiftfield_F2_S_b(global(P_s_36)).
   (* Assertion 'A,X' *)
@@ -81,7 +81,7 @@ Goal Assertion 'A,X' (file frame.i, line 25):
 Let a = Mptr_0[global(L_x_32)].
 Assume {
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Initializer *)
   Init: a = shift_sint8(global(L_b_31), 0).
 }
@@ -93,7 +93,7 @@ Goal Assertion 'A,Y' (file frame.i, line 26):
 Let a = Mptr_0[global(L_x_32)].
 Assume {
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Initializer *)
   Init: a = shift_sint8(global(L_b_31), 0).
   (* Assertion 'A,X' *)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
index d1a36bd6df85721c2bbe1f11da15e714d5bb0b40..d12ad08ff0605a1f2fe73b3aa46ff670b4065553 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/multi_matrix_types.res.oracle
@@ -81,7 +81,7 @@ theory Compound
   
   (* use map.Map *)
   
-  (* use frama_c_wp.memory.Memory *)
+  (* use frama_c_wp.memaddr.MemAddr *)
   
   function shiftfield_F1_S_f (p:addr) : addr = shift p 0
   
@@ -116,6 +116,8 @@ theory Compound
      [Array_uint32 p n (set mint q v)].
      not q = p -> Array_uint32 p n (set mint q v) = Array_uint32 p n mint
   
+  (* use frama_c_wp.memory.Memory *)
+  
   axiom Q_Array_uint32_eqmem_Mint0 :
     forall mint:addr -> int, mint1:addr -> int, n:int, n1:int, p:addr, q:addr
      [Array_uint32 p n mint, eqmem mint mint1 q n1| Array_uint32 p n mint1,
@@ -238,7 +240,7 @@ end
     
     (* use map.Map *)
     
-    (* use frama_c_wp.memory.Memory *)
+    (* use frama_c_wp.memaddr.MemAddr *)
     
     (* use S1_S *)
     
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle
index 9f67668adc8406b1a0f9382b45f032b7216d5f4d..05e2c69bcbb89ddc09111eba69bafec24230938b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle
@@ -5,11 +5,314 @@
 [wp] [Valid] Goal f_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
+---------------------------------------------
+--- Context 'typed_f' Cluster 'Compound' 
+---------------------------------------------
+theory Compound
+  (* use why3.BuiltIn.BuiltIn *)
+  
+  (* use bool.Bool *)
+  
+  (* use int.Int *)
+  
+  (* use int.ComputerDivision *)
+  
+  (* use real.RealInfix *)
+  
+  (* use frama_c_wp.qed.Qed *)
+  
+  (* use map.Map *)
+  
+  (* use frama_c_wp.memaddr.MemAddr *)
+  
+  function shift_sint8 (p:addr) (k:int) : addr = shift p k
+end
+---------------------------------------------
+--- Context 'typed_f' Cluster 'cstring' 
+---------------------------------------------
+theory Cstring
+  (* use why3.BuiltIn.BuiltIn *)
+  
+  (* use bool.Bool *)
+  
+  (* use int.Int *)
+  
+  (* use int.ComputerDivision *)
+  
+  (* use real.RealInfix *)
+  
+  (* use frama_c_wp.qed.Qed *)
+  
+  (* use map.Map *)
+  
+  constant Str_1 : int
+  
+  constant Lit_75AD : int -> int
+  
+  constant Str_2 : int
+  
+  constant Lit_6152 : int -> int
+  
+  constant Str_3 : int
+  
+  constant Str_4 : int
+  
+  constant Lit_7BA4 : int -> int
+  
+  axiom Q_Str_1_base : Str_1 < 0
+  
+  axiom Q_Lit_75AD_literal :
+    (((((get Lit_75AD 0 = 97 /\ get Lit_75AD 1 = 98) /\ get Lit_75AD 2 = 99) /\
+       get Lit_75AD 3 = 100) /\
+      get Lit_75AD 4 = 101) /\
+     get Lit_75AD 5 = 102) /\
+    get Lit_75AD 6 = 0
+  
+  (* use frama_c_wp.memaddr.MemAddr *)
+  
+  axiom Q_Str_1_region : region Str_1 = (- 30125)
+  
+  axiom Q_Str_1_linked : forall t:int -> int. linked t -> get t Str_1 = 7
+  
+  (* use frama_c_wp.memory.Memory *)
+  
+  (* use Compound *)
+  
+  axiom Q_Str_1_literal :
+    forall mchar:addr -> int, i:int.
+     sconst mchar ->
+     get mchar (shift_sint8 (global Str_1) i) = get Lit_75AD i
+  
+  axiom Q_Str_2_base : Str_2 < 0
+  
+  axiom Q_Lit_6152_literal :
+    ((get Lit_6152 0 = 100 /\ get Lit_6152 1 = 101) /\ get Lit_6152 2 = 102) /\
+    get Lit_6152 3 = 0
+  
+  axiom Q_Str_2_region : region Str_2 = (- 24914)
+  
+  axiom Q_Str_2_linked : forall t:int -> int. linked t -> get t Str_2 = 4
+  
+  axiom Q_Str_2_literal :
+    forall mchar:addr -> int, i:int.
+     sconst mchar ->
+     get mchar (shift_sint8 (global Str_2) i) = get Lit_6152 i
+  
+  axiom Q_Str_3_base : Str_3 < 0
+  
+  axiom Q_Str_3_region : region Str_3 = (- 24914)
+  
+  axiom Q_Str_3_linked : forall t:int -> int. linked t -> get t Str_3 = 4
+  
+  axiom Q_Str_3_literal :
+    forall mchar:addr -> int, i:int.
+     sconst mchar ->
+     get mchar (shift_sint8 (global Str_3) i) = get Lit_6152 i
+  
+  axiom Q_Str_4_base : Str_4 < 0
+  
+  axiom Q_Lit_7BA4_literal :
+    ((get Lit_7BA4 0 = 97 /\ get Lit_7BA4 1 = 98) /\ get Lit_7BA4 2 = 99) /\
+    get Lit_7BA4 3 = 0
+  
+  axiom Q_Str_4_region : region Str_4 = (- 31652)
+  
+  axiom Q_Str_4_linked : forall t:int -> int. linked t -> get t Str_4 = 4
+  
+  axiom Q_Str_4_literal :
+    forall mchar:addr -> int, i:int.
+     sconst mchar ->
+     get mchar (shift_sint8 (global Str_4) i) = get Lit_7BA4 i
+end
+[wp:print-generated] 
+  theory WP
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    (* use Cstring *)
+    
+    goal wp_goal : not Str_4 = Str_3
+  end
 [wp] [Valid] typed_f_assert_AB (Alt-Ergo) (Cached)
+[wp:print-generated] 
+  theory WP1
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    (* use Cstring *)
+    
+    goal wp_goal :
+      forall t:int -> int.
+       not Str_4 = Str_3 ->
+       linked t -> valid_rd t (shift_sint8 (global Str_3) 0) 3
+  end
 [wp] [Valid] typed_f_assert_B_valid (Alt-Ergo) (Cached)
+[wp:print-generated] 
+  theory WP2
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    (* use frama_c_wp.memaddr.MemAddr *)
+    
+    (* use Cstring *)
+    
+    (* use frama_c_wp.cint.Cint *)
+    
+    goal wp_goal :
+      let a = global Str_3 in
+      let a1 = shift_sint8 a 3 in
+      forall t:int -> int, t1:addr -> int.
+       let a2 = a in
+       let a3 = a1 in
+       let x = get t1 a3 in
+       not Str_4 = Str_3 ->
+       linked t ->
+       sconst t1 ->
+       is_sint8 x ->
+       valid_rd t (shift_sint8 a2 0) 3 -> x = 0 /\ valid_rd t a3 1
+  end
 [wp] [Valid] typed_f_assert_B_end (Alt-Ergo) (Cached)
+[wp:print-generated] 
+  theory WP3
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    (* use frama_c_wp.memaddr.MemAddr *)
+    
+    (* use Cstring *)
+    
+    goal wp_goal :
+      let a = global Str_3 in
+      let a1 = shift_sint8 a 3 in
+      forall t:int -> int, t1:addr -> int.
+       let a2 = a in
+       let a3 = a1 in
+       not Str_4 = Str_3 ->
+       get t1 a3 = 0 ->
+       linked t ->
+       sconst t1 ->
+       valid_rd t (shift_sint8 a2 0) 3 ->
+       valid_rd t a3 1 -> not valid_rd t (shift_sint8 a2 4) 1
+  end
 [wp] [Valid] typed_f_assert_B_out (Alt-Ergo) (Cached)
+[wp:print-generated] 
+  theory WP4
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    (* use frama_c_wp.memaddr.MemAddr *)
+    
+    (* use Cstring *)
+    
+    goal wp_goal :
+      let a = global Str_3 in
+      let a1 = shift_sint8 a 3 in
+      forall t:int -> int, t1:addr -> int.
+       let a2 = a in
+       let a3 = a1 in
+       not Str_4 = Str_3 ->
+       get t1 a3 = 0 ->
+       linked t ->
+       sconst t1 ->
+       valid_rd t (shift_sint8 a2 0) 3 ->
+       valid_rd t a3 1 ->
+       not valid_rd t (shift_sint8 a2 4) 1 ->
+       not valid_rw t (shift_sint8 a2 1) 1
+  end
 [wp] [Valid] typed_f_assert_B_rw (Alt-Ergo) (Cached)
+[wp:print-generated] 
+  theory WP5
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    (* use frama_c_wp.memaddr.MemAddr *)
+    
+    (* use Cstring *)
+    
+    goal wp_goal :
+      let a = global Str_3 in
+      let a1 = shift_sint8 a 3 in
+      forall t:int -> int, t1:addr -> int, i:int.
+       let a2 = a in
+       let a3 = a1 in
+       not Str_4 = Str_3 ->
+       get t1 a3 = 0 ->
+       0 <= i ->
+       i <= 2 ->
+       linked t ->
+       sconst t1 ->
+       valid_rd t (shift_sint8 a2 0) 3 ->
+       valid_rd t a3 1 ->
+       not valid_rd t (shift_sint8 a2 4) 1 ->
+       not valid_rw t (shift_sint8 a2 1) 1 ->
+       get t1 (shift_sint8 (global Str_1) (3 + i)) = get t1 (shift_sint8 a2 i)
+  end
 [wp] [Valid] typed_f_assert_VAL (Alt-Ergo) (Cached)
 [wp] Proved goals:    8 / 8
   Terminating:     1
diff --git a/src/plugins/wp/tests/wp_typed/unit_string.i b/src/plugins/wp/tests/wp_typed/unit_string.i
index 16e907a20914644ecb17fd5fc4eac077136a5ac2..a5b2006e6f945300028ad455cf625149a0b8d801 100644
--- a/src/plugins/wp/tests/wp_typed/unit_string.i
+++ b/src/plugins/wp/tests/wp_typed/unit_string.i
@@ -1,5 +1,5 @@
 /* run.config_qualif
-   OPT: -wp-literals
+   OPT: -wp-literals -wp-msg-key print-generated
 */
 
 void f(void)
diff --git a/src/plugins/wp/tests/wp_usage/oracle/global.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/global.0.res.oracle
index 564cf3d6ec4468b8f9e6322b4aa1cda2a977d7ee..596f28a8c0dd0200f5ea3914db799a12271663ed 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/global.0.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/global.0.res.oracle
@@ -12,7 +12,7 @@ Goal Assertion 'no_address_taken' (file global.c, line 17):
 Let a = Mptr_0[global(P_a_23)].
 Assume {
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Pre-condition *)
   Have: valid_rw(Malloc_0, a, 1).
 }
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle
index 492892655e7a24f04f8a0aa36f7383688786aec2..78be9b03031296ebcc358cecff7e9a2dafa3ce59 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle
@@ -19,7 +19,7 @@ Let a_4 = shift_uint8(a_3, 0).
 Assume {
   Type: is_sint32(len_0) /\ is_sint32(len_1).
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Goal *)
   When: (0 <= i) /\ ((2 + i) <= len_0).
   (* Pre-condition 'write_access' *)
@@ -54,7 +54,7 @@ Let a_5 = shift_uint8(a_3, i).
 Assume {
   Type: is_sint32(len_0) /\ is_sint32(len_1).
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Goal *)
   When: (0 <= i) /\ ((2 + i) <= len_0).
   (* Pre-condition 'write_access' *)
@@ -89,7 +89,7 @@ Let a_5 = a_2[v <- a_2[v_1]].
 Assume {
   Type: is_sint32(len_0) /\ is_sint32(len_1) /\ is_sint32(len_1 - 1).
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Goal *)
   When: (0 <= i) /\ ((i + len_1) <= len_0).
   (* Pre-condition 'write_access' *)
@@ -140,7 +140,7 @@ Let a_4 = shift_uint8(a_3, 0).
 Assume {
   Type: is_sint32(len_1) /\ is_sint32(len_0) /\ is_sint32(len_0 - 1).
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Pre-condition 'write_access' *)
   Have: valid_rw(Malloc_0, a_1, len_1).
   (* Pre-condition 'read_access' *)
@@ -208,7 +208,7 @@ Let a_7 = shift_uint8(a_6, 0).
 Assume {
   Type: is_sint32(len_0) /\ is_sint32(len_1) /\ is_sint32(len_1 - 1).
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Goal *)
   When: !invalid(Malloc_0[P_src_24 <- 1][P_dst_25 <- 1], v, 1).
   (* Pre-condition 'write_access' *)
@@ -266,7 +266,7 @@ Let a_4 = shift_uint8(a_3, 0).
 Assume {
   Type: is_sint32(len_0) /\ is_sint32(len_1).
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Goal *)
   When: (0 <= i) /\ ((2 + i) <= len_0).
   (* Pre-condition 'write_access' *)
@@ -301,7 +301,7 @@ Let a_5 = shift_uint8(a_3, i).
 Assume {
   Type: is_sint32(len_0) /\ is_sint32(len_1).
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Goal *)
   When: (0 <= i) /\ ((2 + i) <= len_0).
   (* Pre-condition 'write_access' *)
@@ -336,7 +336,7 @@ Let a_5 = a_2[dst2_0 <- a_2[src2_0]].
 Assume {
   Type: is_sint32(len_0) /\ is_sint32(len_1) /\ is_sint32(len_1 - 1).
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Goal *)
   When: (0 <= i) /\ ((i + len_1) <= len_0).
   (* Pre-condition 'write_access' *)
@@ -387,7 +387,7 @@ Let a_4 = shift_uint8(a_3, 0).
 Assume {
   Type: is_sint32(len_1) /\ is_sint32(len_0) /\ is_sint32(len_0 - 1).
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Pre-condition 'write_access' *)
   Have: valid_rw(Malloc_0, a_1, len_1).
   (* Pre-condition 'read_access' *)
@@ -453,7 +453,7 @@ Let a_5 = shift_uint8(a_4, 0).
 Assume {
   Type: is_sint32(len_0) /\ is_sint32(len_1) /\ is_sint32(len_1 - 1).
   (* Heap *)
-  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  Type: linked(Malloc_0) /\ framed(Mptr_0).
   (* Goal *)
   When: !invalid(Malloc_0[P_src_47 <- 1][P_dst_48 <- 1], tmp_0, 1).
   (* Pre-condition 'write_access' *)