diff --git a/src/plugins/wp/MemEmpty.ml b/src/plugins/wp/MemEmpty.ml
index 5435ab551b6dbc7d0894ec12734805e1902134ba..837d3f28f39ba069e34cc8093e574fb97cedc744 100644
--- a/src/plugins/wp/MemEmpty.ml
+++ b/src/plugins/wp/MemEmpty.ml
@@ -43,7 +43,7 @@ let configure () =
let no_binder = { bind = fun _ f v -> f v }
let configure_ia _ = no_binder
-let hypotheses () = []
+let hypotheses p = p
module Chunk =
struct
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 3723ce4232264c2faccafea2a67ae8216a808eab..def850d503eb8b83d717a425f02ed7b9a96b03a3 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -441,7 +441,7 @@ let configure_ia =
let no_binder = { bind = fun _ f v -> f v } in
fun _vertex -> no_binder
-let hypotheses () = []
+let hypotheses p = p
let error msg = Warning.error ~source:"Region Model" msg
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 6743fc7a086ad6307be7534c6fe25eeff69917dd..9ef4f43ed454788eaa4563406a7db23e85e2a166 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -42,7 +42,7 @@ module L = Qed.Logic
(* -------------------------------------------------------------------------- *)
let datatype = "MemTyped"
-let hypotheses () = []
+let hypotheses p = p
let configure () =
begin
let orig_pointer = Context.push Lang.pointer (fun _ -> t_addr) in
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 7a395b0e59ffc8cf1a02eb6546862d6cb7ae0a22..7d07665c6be051830d7e845d42408e405bcaec88 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -52,11 +52,11 @@ struct
let no_binder = { bind = fun _ f v -> f v }
let configure_ia _ = no_binder
- let hypotheses () =
+ let hypotheses p =
let kf,init = match WpContext.get_scope () with
| WpContext.Global -> None,false
| WpContext.Kf f -> Some f, WpStrategy.is_main_init f in
- let w = ref MemoryContext.empty in
+ let w = ref p in
V.iter ?kf ~init (fun vi -> w := MemoryContext.set vi (V.param vi) !w) ;
let add_assign kf _emitter = function
| WritesAny ->
@@ -72,7 +72,7 @@ struct
| Some kf ->
Annotations.iter_assigns (add_assign kf) kf Cil.default_behavior_name
end ;
- MemoryContext.requires !w @ M.hypotheses ()
+ M.hypotheses !w
(* -------------------------------------------------------------------------- *)
(* --- Chunk --- *)
diff --git a/src/plugins/wp/MemZeroAlias.ml b/src/plugins/wp/MemZeroAlias.ml
index 3300bf555d9fc3cc7b45f1d596572499d7510205..3e185883a6dc47ecbf239c9a312ab8b8bbc1efcf 100644
--- a/src/plugins/wp/MemZeroAlias.ml
+++ b/src/plugins/wp/MemZeroAlias.ml
@@ -48,7 +48,7 @@ let no_binder = { bind = fun _ f v -> f v }
let configure_ia _ = no_binder
(* TODO: compute actual separation hypotheses *)
-let hypotheses () = []
+let hypotheses p = p
(* -------------------------------------------------------------------------- *)
(* --- Chunks --- *)
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 98754486ae49dc64946f4e89df963e7d732229e3..bc4f14f098b45db301ab42e55350f05c389df37e 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -291,9 +291,10 @@ sig
val datatype : string
(** For projectification. Must be unique among models. *)
- val hypotheses : unit -> MemoryContext.clause list
- (** Computes the memory model hypotheses including separation and validity
- clauses to be verified for this model. *)
+ val hypotheses : MemoryContext.partition -> MemoryContext.partition
+ (** Computes the memory model partitionning of the memory locations.
+ This function typically adds new elements to the partition received
+ in input (that can be empty). *)
module Chunk : Chunk
(** Memory model chunks. *)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index c350f0f5779d5de2272bee29683161bf140e4290..bb54e4da62830925b1491204604eeed8fb21a66e 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -105,7 +105,8 @@ let wp_warn_memory_context () =
begin
wp_iter_model
begin fun kf m ->
- let hyp = WpContext.compute_hypotheses m kf in
+ let partition = WpContext.compute_hypotheses m kf in
+ let hyp = MemoryContext.requires partition in
if hyp <> [] then
Wp_parameters.warning
~current:false
diff --git a/src/plugins/wp/wpContext.ml b/src/plugins/wp/wpContext.ml
index b37368f1378ab00324b27263dec554cf50b2aa52..acc32631cad27c54f7759b625abc66d6cde26b94 100644
--- a/src/plugins/wp/wpContext.ml
+++ b/src/plugins/wp/wpContext.ml
@@ -34,11 +34,11 @@ type model = {
and rollback = (unit -> unit)
and scope = Global | Kf of Kernel_function.t
-and hypotheses = unit -> MemoryContext.clause list
+and hypotheses = MemoryContext.partition -> MemoryContext.partition
and context = model * scope
and t = context
-let nohyp (_kf) = []
+let nohyp (_kf) = MemoryContext.empty
module MODEL =
struct
@@ -149,7 +149,8 @@ let get_context () = Context.get context |> snd
let get_model () = get_context () |> fst
let get_scope () = get_context () |> snd
-let compute_hypotheses m f = on_context (m,Kf f) m.hypotheses ()
+let compute_hypotheses m f =
+ on_context (m,Kf f) m.hypotheses MemoryContext.empty
let directory () = get_model () |> MODEL.id |> Wp_parameters.get_output_dir
diff --git a/src/plugins/wp/wpContext.mli b/src/plugins/wp/wpContext.mli
index 7693815595f66aa61dc739c8059173b0a812c50f..a52c5af5f7fbde050c2b4f0b6ec0fb65e5177a89 100644
--- a/src/plugins/wp/wpContext.mli
+++ b/src/plugins/wp/wpContext.mli
@@ -25,7 +25,7 @@
type model
type scope = Global | Kf of Kernel_function.t
type rollback = unit -> unit
-type hypotheses = unit -> MemoryContext.clause list
+type hypotheses = MemoryContext.partition -> MemoryContext.partition
val register :
id:string ->
@@ -44,7 +44,7 @@ val register :
val get_descr : model -> string
val get_emitter : model -> Emitter.t
-val compute_hypotheses : model -> Kernel_function.t -> MemoryContext.clause list
+val compute_hypotheses : model -> Kernel_function.t -> MemoryContext.partition
type context = model * scope
type t = context